Theory: ring

Theorems

EXISTS_ring

⊢ ∀P. (∃r. P r) ⇔ ∃f m0 m. P <|carrier := f; sum := m0; prod := m|>

FORALL_ring

⊢ ∀P. (∀r. P r) ⇔ ∀f m0 m. P <|carrier := f; sum := m0; prod := m|>

LIST_REL_ring_associates_product

⊢ Ring r ⇒
  ∀l1 l2.
    LIST_REL rassoc l1 l2 ∧ set l2 ⊆ R ⇒
    rassoc (GBAG r.prod (LIST_TO_BAG l1)) (GBAG r.prod (LIST_TO_BAG l2))

WHILE_RULE_PRE_POST

⊢ (∀x. Invariant x ∧ Guard x ⇒ f (Cmd x) < f x) ∧
  (∀x. Precond x ⇒ Invariant x) ∧
  (∀x. Invariant x ∧ ¬Guard x ⇒ Postcond x) ∧
  HOARE_SPEC (λx. Invariant x ∧ Guard x) Cmd Invariant ⇒
  HOARE_SPEC Precond (WHILE Guard Cmd) Postcond

ZN_1_exp

⊢ ∀n k. (ZN 1).prod.exp n k = 0

ZN_card

⊢ ∀n. CARD (ZN n).carrier = n

ZN_char

⊢ ∀n. 0 < n ⇒ char (ZN n) = n

ZN_coprime_euler_element

⊢ ∀m n. 1 < m ∧ coprime m n ⇒ n MOD m ∈ Euler m

ZN_coprime_exp_mod

⊢ ∀m n.
    0 < m ∧ coprime m n ⇒ ∀k. n ** k MOD m = n ** (k MOD ordz m n) MOD m

ZN_coprime_invertible

⊢ ∀m n. 1 < m ∧ coprime m n ⇒ Unit (ZN m) (n MOD m)

ZN_coprime_order

⊢ ∀m n. 0 < m ∧ coprime m n ⇒ 0 < ordz m n ∧ n ** ordz m n MOD m = 1 MOD m

ZN_coprime_order_alt

⊢ ∀m n. 1 < m ∧ coprime m n ⇒ 0 < ordz m n ∧ n ** ordz m n MOD m = 1

ZN_coprime_order_divides_phi

⊢ ∀m n. 0 < m ∧ coprime m n ⇒ ordz m n divides phi m

ZN_coprime_order_divides_totient

⊢ ∀m n. 0 < m ∧ coprime m n ⇒ ordz m n divides totient m

ZN_coprime_order_gt_1

⊢ ∀m n. 1 < m ∧ 1 < n MOD m ∧ coprime m n ⇒ 1 < ordz m n

ZN_coprime_order_lt

⊢ ∀m n. 1 < m ∧ coprime m n ⇒ ordz m n < m

ZN_eval

⊢ ∀n. (ZN n).carrier = count n ∧ (ZN n).sum = add_mod n ∧
      (ZN n).prod = times_mod n

ZN_exp

⊢ ∀n. 0 < n ⇒ ∀x k. (ZN n).prod.exp x k = x ** k MOD n

ZN_finite

⊢ ∀n. FINITE (ZN n).carrier

ZN_finite_ring

⊢ ∀n. 0 < n ⇒ FiniteRing (ZN n)

ZN_ids

⊢ ∀n. 0 < n ⇒ (ZN n).sum.id = 0 ∧ (ZN n).prod.id = 1 MOD n

ZN_ids_alt

⊢ ∀n. 1 < n ⇒ (ZN n).sum.id = 0 ∧ (ZN n).prod.id = 1

ZN_invertibles

⊢ ∀n. 1 < n ⇒ Invertibles (ZN n).prod = Estar n

ZN_invertibles_finite_group

⊢ ∀n. 0 < n ⇒ FiniteGroup (Invertibles (ZN n).prod)

ZN_invertibles_group

⊢ ∀n. 0 < n ⇒ Group (Invertibles (ZN n).prod)

ZN_invertibles_order

⊢ ∀m n. 0 < m ⇒ order (Invertibles (ZN m).prod) (n MOD m) = ordz m n

ZN_mult_inv_coprime

⊢ ∀n. 0 < n ⇒ ∀x y. x * y MOD n = 1 ⇒ coprime x n

ZN_mult_inv_coprime_iff

⊢ ∀n. 1 < n ⇒ ∀x. coprime x n ⇔ ∃y. x * y MOD n = 1

ZN_not_coprime

⊢ ∀m n. 0 < m ∧ gcd m n ≠ 1 ⇒ ∀k. 0 < k ⇒ n ** k MOD m ≠ 1

ZN_num

⊢ ∀n. 0 < n ⇒ ∀k. (ZN n).sum.exp 1 k = k MOD n

ZN_num_0

⊢ ∀n c. 0 < n ⇒ (ZN n).sum.exp 0 c = 0

ZN_num_1

⊢ ∀n. (ZN n).sum.exp (ZN n).prod.id 1 = 1 MOD n

ZN_num_mod

⊢ ∀n c. 0 < n ⇒ (ZN n).sum.exp (ZN n).prod.id c = c MOD n

ZN_order_0

⊢ ∀n. 0 < n ⇒ ordz n 0 = if n = 1 then 1 else 0

ZN_order_1

⊢ ∀n. 0 < n ⇒ ordz n 1 = 1

ZN_order_divides_exp

⊢ ∀m n k. 1 < m ∧ 0 < k ⇒ (n ** k MOD m = 1 ⇔ ordz m n divides k)

ZN_order_divides_phi

⊢ ∀m n. 0 < m ∧ 0 < ordz m n ⇒ ordz m n divides phi m

ZN_order_divides_tops_index

⊢ ∀n j k. 1 < n ∧ 0 < j ∧ 1 < k ⇒ (k divides tops n j ⇔ ordz k n divides j)

ZN_order_divisibility

⊢ ∀m n. 0 < m ⇒ m divides tops n (ordz m n)

ZN_order_eq_0

⊢ ∀m n. 0 < m ⇒ (ordz m n = 0 ⇔ gcd m n ≠ 1)

ZN_order_eq_0_iff

⊢ ∀m n. 1 < m ⇒ (ordz m n = 0 ⇔ ∀k. 0 < k ⇒ n ** k MOD m ≠ 1)

ZN_order_eq_0_test

⊢ ∀m n. 1 < m ⇒ (ordz m n = 0 ⇔ ∀j. 0 < j ∧ j < m ⇒ n ** j MOD m ≠ 1)

ZN_order_eq_1

⊢ ∀m n. 0 < m ⇒ (ordz m n = 1 ⇔ n MOD m = 1 MOD m)

ZN_order_eq_1_alt

⊢ ∀m n. 1 < m ⇒ (ordz m n = 1 ⇔ n MOD m = 1)

ZN_order_eq_1_by_prime_factors

⊢ ∀m n.
    0 < m ∧ coprime m n ∧ (∀p. prime p ∧ p divides n ⇒ ordz m p = 1) ⇒
    ordz m n = 1

ZN_order_gt_1_property

⊢ ∀m n. 0 < m ∧ 1 < ordz m n ⇒ ∃p. prime p ∧ p divides n ∧ 1 < ordz m p

ZN_order_le

⊢ ∀m n. 0 < m ⇒ ordz m n ≤ m

ZN_order_le_tops_index

⊢ ∀n j k. 1 < n ∧ 0 < j ∧ 1 < k ∧ k divides tops n j ⇒ ordz k n ≤ j

ZN_order_lt

⊢ ∀k n m. 0 < k ∧ k < m ⇒ ordz k n < m

ZN_order_minimal

⊢ ∀m n k. 0 < m ∧ 0 < k ∧ k < ordz m n ⇒ n ** k MOD m ≠ 1

ZN_order_mod

⊢ ∀m n. 0 < m ⇒ ordz m (n MOD m) = ordz m n

ZN_order_mod_1

⊢ ∀n. ordz 1 n = 1

ZN_order_nonzero

⊢ ∀m n. 0 < m ⇒ (ordz m n ≠ 0 ⇔ coprime m n)

ZN_order_nonzero_iff

⊢ ∀m n. 1 < m ⇒ (ordz m n ≠ 0 ⇔ ∃k. 0 < k ∧ n ** k MOD m = 1)

ZN_order_property

⊢ ∀m n. 0 < m ⇒ n ** ordz m n MOD m = 1 MOD m

ZN_order_property_alt

⊢ ∀m n. 1 < m ⇒ n ** ordz m n MOD m = 1

ZN_order_test_1

⊢ ∀m n k.
    1 < m ∧ 0 < k ⇒
    (ordz m n = k ⇔ n ** k MOD m = 1 ∧ ∀j. 0 < j ∧ j < k ⇒ n ** j MOD m ≠ 1)

ZN_order_test_2

⊢ ∀m n k.
    1 < m ∧ 0 < k ⇒
    (ordz m n = k ⇔
     n ** k MOD m = 1 ∧
     ∀j. 0 < j ∧ j < k ∧ j divides phi m ⇒ n ** j MOD m ≠ 1)

ZN_order_test_3

⊢ ∀m n k.
    1 < m ∧ 0 < k ⇒
    (ordz m n = k ⇔
     k divides phi m ∧ n ** k MOD m = 1 ∧
     ∀j. 0 < j ∧ j < k ∧ j divides phi m ⇒ n ** j MOD m ≠ 1)

ZN_order_test_4

⊢ ∀m n k.
    1 < m ⇒
    (ordz m n = k ⇔
     n ** k MOD m = 1 ∧
     ∀j. 0 < j ∧ j < (if k = 0 then m else k) ⇒ n ** j MOD m ≠ 1)

ZN_order_test_propery

⊢ ∀m n k.
    1 < m ∧ 0 < k ∧ n ** k MOD m = 1 ∧
    (∀j. 0 < j ∧ j < k ∧ j divides phi m ⇒ n ** j MOD m ≠ 1) ⇒
    ∀j. 0 < j ∧ j < k ∧ ¬(j divides phi m) ⇒
        ordz m n = k ∨ n ** j MOD m ≠ 1

ZN_order_upper

⊢ ∀m n. 0 < m ⇒ ordz m n ≤ phi m

ZN_order_with_coprime_1

⊢ ∀m n. 1 < n ∧ coprime m n ∧ 1 < ordz m n ⇒ 1 < m

ZN_order_with_coprime_2

⊢ ∀m n k. 1 < m ∧ m divides n ∧ 1 < ordz k m ∧ coprime k n ⇒ 1 < n ∧ 1 < k

ZN_property

⊢ ∀n. (∀x. x ∈ (ZN n).carrier ⇔ x < n) ∧ (ZN n).sum.id = 0 ∧
      (ZN n).prod.id = (if n = 1 then 0 else 1) ∧
      (∀x y. (ZN n).sum.op x y = (x + y) MOD n) ∧
      (∀x y. (ZN n).prod.op x y = x * y MOD n) ∧ FINITE (ZN n).carrier ∧
      CARD (ZN n).carrier = n

ZN_ring

⊢ ∀n. 0 < n ⇒ Ring (ZN n)

ZN_to_ZN_element

⊢ ∀n m x. 0 < m ∧ x ∈ (ZN n).carrier ⇒ x MOD m ∈ (ZN m).carrier

ZN_to_ZN_prod_monoid_homo

⊢ ∀n m.
    0 < n ∧ m divides n ⇒ MonoidHomo (λx. x MOD m) (ZN n).prod (ZN m).prod

ZN_to_ZN_ring_homo

⊢ ∀n m. 0 < n ∧ m divides n ⇒ RingHomo (λx. x MOD m) (ZN n) (ZN m)

ZN_to_ZN_sum_group_homo

⊢ ∀n m. 0 < n ∧ m divides n ⇒ GroupHomo (λx. x MOD m) (ZN n).sum (ZN m).sum

ZP_finite

⊢ ∀p. FINITE (ZP p).carrier

ZP_finite_integral_domain

⊢ ∀p. prime p ⇒ FiniteIntegralDomain (ZP p)

ZP_integral_domain

⊢ ∀p. prime p ⇒ IntegralDomain (ZP p)

Z_add_abelian_group

⊢ AbelianGroup Z_add

Z_add_group

⊢ Group Z_add

Z_add_inv

⊢ ∀z. z ∈ Z_add.carrier ⇒ Z_add.inv z = -z

Z_euclid_ring

⊢ EuclideanRing Z Num

Z_ideal_map_bij

⊢ ∀n. 0 < n ⇒
      BIJ (λj. coset Z.sum (&j) (Z* n).sum.carrier) (ZN n).carrier
        (Z / Z* n).carrier

Z_ideal_map_element

⊢ ∀n j.
    0 < n ∧ j ∈ (ZN n).carrier ⇒
    coset Z.sum (&j) (Z* n).sum.carrier ∈ (Z / Z* n).carrier

Z_ideal_map_group_homo

⊢ ∀n. 0 < n ⇒
      GroupHomo (λj. coset Z.sum (&j) (Z* n).sum.carrier) (ZN n).sum
        (Z / Z* n).sum

Z_ideal_map_monoid_homo

⊢ ∀n. 0 < n ⇒
      MonoidHomo (λj. coset Z.sum (&j) (Z* n).sum.carrier) (ZN n).prod
        (Z / Z* n).prod

Z_ideal_sum_group

⊢ ∀n. Group (Z* n).sum

Z_ideal_sum_normal

⊢ ∀n. (Z* n).sum << Z.sum

Z_ideal_sum_subgroup

⊢ ∀n. (Z* n).sum ≤ Z.sum

Z_ideal_thm

⊢ ∀n. Z* n << Z

Z_mult_abelian_monoid

⊢ AbelianMonoid Z_mult

Z_mult_monoid

⊢ Monoid Z_mult

Z_multiple_less_neg_eq

⊢ ∀n x y. 0 < n ∧ x < n ∧ y < n ∧ -&x + &y ∈ Z_multiple n ⇒ x = y

Z_principal_ideal_ring

⊢ PrincipalIdealRing Z

Z_quotient_iso_ZN

⊢ ∀n. 0 < n ⇒
      RingIso (λj. coset Z.sum (&j) (Z* n).sum.carrier) (ZN n) (Z / Z* n)

Z_ring

⊢ Ring Z

Z_sum_cogen

⊢ ∀n. 0 < n ⇒
      ∀x. x ∈ Z.sum.carrier ⇒
          ∃y. cogen Z.sum (Z* n).sum (coset Z.sum x (Z* n).sum.carrier) =
              x + &n * y

Z_sum_coset_eq

⊢ ∀n. 0 < n ⇒
      ∀p. coset Z.sum p (Z* n).sum.carrier =
          coset Z.sum (p % &n) (Z* n).sum.carrier

char_eq_0

⊢ ∀r. char r = 0 ⇔ ∀n. 0 < n ⇒ ##n ≠ #0

char_minimal

⊢ ∀r. 0 < char r ⇒ ∀n. 0 < n ∧ n < char r ⇒ ##n ≠ #0

char_property

⊢ ∀r. ##(char r) = #0

compute_ordz_0

⊢ ∀n. compute_ordz 0 n = ordz 0 n

compute_ordz_1

⊢ ∀n. compute_ordz 1 n = 1

compute_ordz_eqn

⊢ ∀m n. compute_ordz m n = ordz m n

compute_ordz_hoare

⊢ ∀m n.
    1 < m ∧ coprime m n ⇒
    HOARE_SPEC (λi. 0 < i ∧ i ≤ ordz m n)
      (WHILE (λi. n ** i MOD m ≠ 1) SUC) (λi. i = ordz m n)

datatype_ring

⊢ DATATYPE (record ring carrier sum prod)

euclid_ring_map

⊢ ∀r f. EuclideanRing r f ⇒ ∀x. f x = 0 ⇔ x = #0

euclid_ring_principal_ideal_ring

⊢ ∀r f. EuclideanRing r f ⇒ PrincipalIdealRing r

euclid_ring_property

⊢ ∀r f.
    EuclideanRing r f ⇒
    ∀x y.
      x ∈ R ∧ y ∈ R ∧ y ≠ #0 ⇒
      ∃q t. q ∈ R ∧ t ∈ R ∧ x = q * y + t ∧ f t < f y

euclid_ring_ring

⊢ ∀r f. EuclideanRing r f ⇒ Ring r

finite_integral_domain_nonzero_group

⊢ ∀r. FiniteIntegralDomain r ⇒ Group f*

finite_integral_domain_nonzero_invertible

⊢ ∀r. FiniteIntegralDomain r ⇒ monoid_invertibles r.prod = R+

finite_integral_domain_nonzero_invertible_alt

⊢ ∀r. FiniteIntegralDomain r ⇒ monoid_invertibles f* = F*

finite_integral_domain_period_exists

⊢ ∀r. FiniteIntegralDomain r ⇒ ∀x. x ∈ R+ ⇒ ∃k. 0 < k ∧ x ** k = #1

finite_ring_add_finite_abelian_group

⊢ ∀r. FiniteRing r ⇒ FiniteAbelianGroup r.sum ∧ r.sum.carrier = R

finite_ring_add_finite_group

⊢ ∀r. FiniteRing r ⇒ FiniteGroup r.sum ∧ r.sum.carrier = R

finite_ring_card_eq_1

⊢ ∀r. FiniteRing r ⇒ (CARD R = 1 ⇔ #1 = #0)

finite_ring_card_pos

⊢ ∀r. FiniteRing r ⇒ 0 < CARD R

finite_ring_card_prime

⊢ ∀r. FiniteRing r ∧ prime (CARD R) ⇒ char r = CARD R

finite_ring_char

⊢ ∀r. FiniteRing r ⇒ 0 < char r ∧ char r = order r.sum #1

finite_ring_char_alt

⊢ ∀r. FiniteRing r ⇒
      ∀n. char r = n ⇔ 0 < n ∧ ##n = #0 ∧ ∀m. 0 < m ∧ m < n ⇒ ##m ≠ #0

finite_ring_char_divides

⊢ ∀r. FiniteRing r ⇒ char r divides CARD R

finite_ring_char_pos

⊢ ∀r. FiniteRing r ⇒ 0 < char r

finite_ring_is_ring

⊢ ∀r. FiniteRing r ⇒ Ring r

finite_ring_mult_finite_abelian_monoid

⊢ ∀r. FiniteRing r ⇒ FiniteAbelianMonoid r.prod

finite_ring_mult_finite_monoid

⊢ ∀r. FiniteRing r ⇒ FiniteMonoid r.prod

homo_ring_by_inj

⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ RingHomo f r (homo_ring r f)

homo_ring_property

⊢ ∀r f.
    fR = IMAGE f R ∧ (homo_ring r f).sum = homo_group r.sum f ∧
    (homo_ring r f).prod = homo_group r.prod f

homo_ring_ring

⊢ ∀r f. Ring r ∧ RingHomo f r (homo_ring r f) ⇒ Ring (homo_ring r f)

homo_ring_subring

⊢ ∀r s f. (r ~r~ s) f ⇒ subring (homo_ring r f) s

ideal_antisym

⊢ ∀r i. i << r ∧ r << i ⇒ i = r

ideal_carrier_sing

⊢ ∀r i. Ring r ∧ i << r ⇒ (SING I ⇔ i = <#0>)

ideal_carriers

⊢ ∀r i. i << r ⇒ i.sum.carrier = I ∧ i.prod.carrier = I

ideal_cogen_property

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R/I ⇒ gen x ∈ R ∧ gen x ∘ I = x

ideal_congruence_elements

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ I ∧ y ∈ R ⇒ (y ∈ I ⇔ x === y)

ideal_congruence_equiv

⊢ ∀r i. Ring r ∧ i << r ⇒ $=== equiv_on R

ideal_congruence_iff_inCoset

⊢ ∀r i.
    Ring r ∧ i << r ⇒
    ∀x y. x ∈ I ∧ y ∈ I ⇒ (x === y ⇔ inCoset r.sum i.sum x y)

ideal_congruence_mult

⊢ ∀r i.
    Ring r ∧ i << r ⇒
    ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x === y ⇒ z * x === z * y

ideal_congruence_refl

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R ⇒ x === x

ideal_congruence_sym

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (x === y ⇔ y === x)

ideal_congruence_trans

⊢ ∀r i.
    Ring r ∧ i << r ⇒
    ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x === y ∧ y === z ⇒ x === z

ideal_coset_add

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x ∘ I + y ∘ I = (x + y) ∘ I

ideal_coset_element

⊢ ∀r i x. Ring r ∧ i << r ∧ x ∈ R ⇒ ∀z. z ∈ x ∘ I ⇔ ∃y. y ∈ I ∧ z = x + y

ideal_coset_eq

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (x ∘ I = y ∘ I ⇔ x − y ∈ I)

ideal_coset_eq_carrier

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R ∧ x ∘ I = I ⇔ x ∈ I

ideal_coset_eq_congruence

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (x ∘ I = y ∘ I ⇔ x === y)

ideal_coset_has_gen_diff

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R ⇒ gen (x ∘ I) − x ∈ I

ideal_coset_mult

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x ∘ I * y ∘ I = (x * y) ∘ I

ideal_coset_neg

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R ⇒ x ∘ I + -x ∘ I = I

ideal_coset_of_element

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ I ⇒ x ∘ I = I

ideal_coset_property

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R ⇒ x ∘ I ∈ R/I ∧ gen (x ∘ I) ∘ I = x ∘ I

ideal_coset_zero

⊢ ∀r i. Ring r ∧ i << r ⇒ #0 ∘ I = I

ideal_element

⊢ ∀r i. i << r ⇒ ∀x. x ∈ I ⇒ x ∈ r.sum.carrier

ideal_element_property

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ I ⇒ x ∈ R

ideal_eq_ideal

⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ (i = j ⇔ I = J)

ideal_gen_exists

⊢ ∀r i.
    Ring r ∧ i << r ∧ i ≠ <#0> ⇒
    ∀f. (∀x. f x = 0 ⇔ x = #0) ⇒
        ∃p. p ∈ I ∧ p ≠ #0 ∧ ∀z. z ∈ I ∧ z ≠ #0 ⇒ f p ≤ f z

ideal_gen_minimal

⊢ ∀r i.
    Ring r ∧ i << r ∧ i ≠ <#0> ⇒
    ∀f. (∀x. f x = 0 ⇔ x = #0) ⇒
        ∀z. z ∈ I ⇒ (f z < f (ideal_gen r i f) ⇔ z = #0)

ideal_has_diff

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ I ∧ y ∈ I ⇒ x − y ∈ I

ideal_has_multiple

⊢ ∀r i. i << r ⇒ ∀x y. x ∈ I ∧ y ∈ R ⇒ x * y ∈ I

ideal_has_neg

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ I ⇒ -x ∈ I

ideal_has_one

⊢ ∀r i. Ring r ∧ i << r ∧ #1 ∈ I ⇒ I = R

ideal_has_principal_ideal

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀p. p ∈ R ⇒ (p ∈ I ⇔ <p> << i)

ideal_has_product

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ I ∧ y ∈ I ⇒ x * y ∈ I

ideal_has_subgroup

⊢ ∀r i. i << r ⇒ i.sum ≤ r.sum

ideal_has_sum

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ I ∧ y ∈ I ⇒ x + y ∈ I

ideal_has_zero

⊢ ∀r i. Ring r ∧ i << r ⇒ #0 ∈ I

ideal_in_quotient_ring

⊢ ∀r i. Ring r ∧ i << r ⇒ I ∈ R/I

ideal_ops

⊢ ∀r i. i << r ⇒ i.sum.op = $+ ∧ i.prod.op = $*

ideal_product_property

⊢ ∀r i. i << r ⇒ ∀x y. x ∈ I ∧ y ∈ R ⇒ x * y ∈ I ∧ y * x ∈ I

ideal_property

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ I ∧ y ∈ I ⇒ x + y ∈ I ∧ x * y ∈ I

ideal_refl

⊢ ∀r. Ring r ⇒ r << r

ideal_sub_ideal

⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ (i << j ⇔ I ⊆ J)

ideal_sub_itself

⊢ ∀r i. Ring r ∧ i << r ⇒ i << i

ideal_subgroup_ideal_sum

⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ i.sum ≤ (i + j).sum

ideal_sum_comm

⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ i + j = j + i

ideal_sum_element

⊢ ∀i j x. x ∈ (i + j).carrier ⇔ ∃y z. y ∈ I ∧ z ∈ J ∧ x = y + z

ideal_sum_group

⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ Group (i + j).sum

ideal_sum_has_ideal

⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ i << (i + j)

ideal_sum_has_ideal_comm

⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ j << (i + j)

ideal_sum_ideal

⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ (i + j) << r

ideal_sum_sub_ideal

⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ ((i + j) << j ⇔ i << j)

ideal_sum_subgroup

⊢ ∀r i j. Ring r ∧ i << r ∧ j << r ⇒ (i + j).sum ≤ r.sum

ideal_with_one

⊢ ∀r. Ring r ⇒ ∀i. i << r ∧ #1 ∈ I ⇔ i = r

ideal_with_unit

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ I ∧ unit x ⇒ i = r

ideal_zero

⊢ ∀r i. Ring r ∧ i << r ⇒ i.sum.id = #0

integral_domain_char

⊢ ∀r. IntegralDomain r ⇒ char r = 0 ∨ prime (char r)

integral_domain_divides_prime

⊢ ∀r p x.
    IntegralDomain r ∧ x ∈ R ∧ p ∈ R ∧ p ≠ #0 ∧ rprime p ∧ p ∉ R* ∧
    x ∉ R* ∧ x rdivides p ⇒
    rassoc x p

integral_domain_exp_eq

⊢ ∀r. IntegralDomain r ⇒
      ∀x. x ∈ R+ ⇒ ∀m n. m < n ∧ x ** m = x ** n ⇒ x ** (n − m) = #1

integral_domain_exp_eq_zero

⊢ ∀r. IntegralDomain r ⇒ ∀x. x ∈ R ⇒ ∀n. x ** n = #0 ⇔ n ≠ 0 ∧ x = #0

integral_domain_exp_nonzero

⊢ ∀r. IntegralDomain r ⇒ ∀x. x ∈ R+ ⇒ ∀n. x ** n ∈ R+

integral_domain_is_ring

⊢ ∀r. IntegralDomain r ⇒ Ring r

integral_domain_mult_eq_zero

⊢ ∀r. IntegralDomain r ⇒
      ∀x y. x ∈ R ∧ y ∈ R ⇒ (x * y = #0 ⇔ x = #0 ∨ y = #0)

integral_domain_mult_lcancel

⊢ ∀r. IntegralDomain r ⇒
      ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (x * y = x * z ⇔ x = #0 ∨ y = z)

integral_domain_mult_nonzero

⊢ ∀r. IntegralDomain r ⇒ ∀x y. x ∈ R+ ∧ y ∈ R+ ⇒ x * y ∈ R+

integral_domain_mult_rcancel

⊢ ∀r. IntegralDomain r ⇒
      ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (y * x = z * x ⇔ x = #0 ∨ y = z)

integral_domain_nonzero_monoid

⊢ ∀r. IntegralDomain r ⇒ Monoid f*

integral_domain_nonzero_mult_carrier

⊢ ∀r. IntegralDomain r ⇒ F* = R+

integral_domain_nonzero_mult_is_monoid

⊢ ∀r. IntegralDomain r ⇒ Monoid (monoid_of_ring_nonzero_mult r)

integral_domain_nonzero_mult_property

⊢ ∀r. IntegralDomain r ⇒ F* = R+ ∧ f*.id = #1 ∧ f*.op = $* ∧ f*.exp = $**

integral_domain_nonzero_order

⊢ ∀r. IntegralDomain r ⇒ ∀x. order r.prod x = order f* x

integral_domain_one_ne_zero

⊢ ∀r. IntegralDomain r ⇒ #1 ≠ #0

integral_domain_one_nonzero

⊢ ∀r. IntegralDomain r ⇒ #1 ∈ R+

integral_domain_order_eq_0

⊢ ∀r. FiniteIntegralDomain r ⇒ ∀x. x ∈ R ⇒ (order f* x = 0 ⇔ x = #0)

integral_domain_order_nonzero

⊢ ∀r. FiniteIntegralDomain r ⇒ ∀x. x ∈ R+ ⇒ order f* x ≠ 0

integral_domain_order_zero

⊢ ∀r. IntegralDomain r ⇒ order f* #0 = 0

integral_domain_prime_factors_unique

⊢ IntegralDomain r ⇒
  ∀l1 l2.
    (∀m. MEM m l1 ⇒ m ∈ R ∧ rprime m ∧ m ≠ #0 ∧ m ∉ R* ) ∧
    (∀m. MEM m l2 ⇒ m ∈ R ∧ rprime m ∧ m ≠ #0 ∧ m ∉ R* ) ∧
    rassoc (GBAG r.prod (LIST_TO_BAG l1)) (GBAG r.prod (LIST_TO_BAG l2)) ⇒
    ∃l3. PERM l2 l3 ∧ LIST_REL rassoc l1 l3

integral_domain_ring_iso

⊢ IntegralDomain r ∧ Ring s ∧ RingIso f r s ⇒ IntegralDomain s

integral_domain_zero_not_unit

⊢ ∀r. IntegralDomain r ⇒ #0 ∉ R*

integral_domain_zero_product

⊢ ∀r. IntegralDomain r ⇒
      ∀x y. x ∈ R ∧ y ∈ R ⇒ (x * y = #0 ⇔ x = #0 ∨ y = #0)

irreducible_associates

⊢ ∀r. Ring r ∧ #1 ≠ #0 ⇒ ∀p s. p ∈ R ∧ unit s ⇒ (atom p ⇔ atom (s * p))

irreducible_element

⊢ ∀r p. atom p ⇒ p ∈ R

irreducible_factors

⊢ ∀r z.
    atom z ⇒
    z ∈ R+ ∧ z ∉ R* ∧ ∀p. p ∈ R ∧ p rdivides z ⇒ rassoc z p ∨ unit p

kernel_ideal_element

⊢ ∀r r_ f x.
    x ∈ (kernel_ideal f r r_).carrier ⇔ x ∈ r.sum.carrier ∧ f x = #0_

kernel_ideal_gen_add_map

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒
    (let
       i = kernel_ideal f r r_
     in
       ∀x y.
         x ∈ R/I ∧ y ∈ R/I ⇒
         f (gen ((gen x + gen y) ∘ I)) = f (gen x) +_ f (gen y))

kernel_ideal_gen_id_map

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒ (let i = kernel_ideal f r r_ in f (gen (#1 ∘ I)) = #1_)

kernel_ideal_gen_mult_map

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒
    (let
       i = kernel_ideal f r r_
     in
       ∀x y.
         x ∈ R/I ∧ y ∈ R/I ⇒
         f (gen ((gen x * gen y) ∘ I)) = f (gen x) *_ f (gen y))

kernel_ideal_quotient_bij

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒
    (let i = kernel_ideal f r r_ in BIJ (f ∘ gen) R/I (IMAGE f R))

kernel_ideal_quotient_element_eq

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒
    (let
       i = kernel_ideal f r r_
     in
       ∀x y. x ∈ R/I ∧ y ∈ R/I ⇒ (gen x − gen y ∈ I ⇔ x = y))

kernel_ideal_quotient_homo

⊢ ∀r s f.
    (r ~r~ s) f ⇒
    (let
       i = kernel_ideal f r s
     in
       RingHomo (f ∘ gen) (r / i) (ring_homo_image f r s))

kernel_ideal_quotient_inj

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒
    (let i = kernel_ideal f r r_ in INJ (f ∘ gen) R/I (IMAGE f R))

kernel_ideal_quotient_iso

⊢ ∀r s f.
    (r ~r~ s) f ⇒
    (let
       i = kernel_ideal f r s
     in
       RingIso (f ∘ gen) (r / i) (ring_homo_image f r s))

kernel_ideal_quotient_surj

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒
    (let i = kernel_ideal f r r_ in SURJ (f ∘ gen) R/I (IMAGE f R))

kernel_ideal_sum_eqn

⊢ ∀r s f. (kernel_ideal f r s).sum = kernel_group f r.sum s.sum

ordz_eval

⊢ ∀m n. order (times_mod m) n = compute_ordz m n

prime_is_irreducible

⊢ ∀r p. IntegralDomain r ∧ p ∈ R ∧ rprime p ∧ p ≠ #0 ∧ p ∉ R* ⇒ atom p

principal_ideal_element

⊢ ∀p x. x ∈ <p>.carrier ⇔ ∃z. z ∈ R ∧ x = p * z

principal_ideal_element_divides

⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ ∀x. x ∈ <p>.carrier ⇔ p rdivides x

principal_ideal_eq_principal_ideal

⊢ ∀r. Ring r ⇒ ∀p q u. p ∈ R ∧ q ∈ R ∧ unit u ∧ p = q * u ⇒ <p> = <q>

principal_ideal_equal_principal_ideal

⊢ ∀r. IntegralDomain r ⇒
      ∀p q. p ∈ R ∧ q ∈ R ⇒ (<p> = <q> ⇔ ∃u. unit u ∧ p = q * u)

principal_ideal_group

⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ Group <p>.sum

principal_ideal_has_element

⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ p ∈ <p>.carrier

principal_ideal_has_principal_ideal

⊢ ∀r. Ring r ⇒ ∀p q. p ∈ R ∧ q ∈ <p>.carrier ⇒ <q> << <p>

principal_ideal_ideal

⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ <p> << r

principal_ideal_property

⊢ ∀r p.
    <p>.carrier = p * R ∧ <p>.sum.carrier = p * R ∧
    <p>.prod.carrier = p * R ∧ <p>.sum.op = $+ ∧ <p>.prod.op = $* ∧
    <p>.sum.id = #0 ∧ <p>.prod.id = #1

principal_ideal_ring_atom_is_prime

⊢ ∀r. PrincipalIdealRing r ⇒ ∀p. atom p ⇒ rprime p

principal_ideal_ring_ideal_maximal

⊢ ∀r. PrincipalIdealRing r ⇒ ∀p. atom p ⇒ maxi <p>

principal_ideal_ring_irreducible_is_prime

⊢ ∀r. PrincipalIdealRing r ⇒ ∀p. atom p ⇒ rprime p

principal_ideal_sub_implies_divides

⊢ ∀r. Ring r ⇒ ∀p q. p ∈ R ∧ q ∈ R ⇒ (q rdivides p ⇔ <p> << <q>)

principal_ideal_subgroup

⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ <p>.sum ≤ r.sum

principal_ideal_subgroup_normal

⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ <p>.sum << r.sum

principal_ideal_sum_eq_ideal

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀p. p ∈ I ⇒ <p> + i = i

principal_ideal_sum_equal_ideal

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀p. p ∈ I ⇔ p ∈ R ∧ <p> + i = i

quotient_ring_add_abelian_group

⊢ ∀r. Ring r ∧ i << r ⇒ AbelianGroup (quotient_ring_add r i)

quotient_ring_add_assoc

⊢ ∀r i.
    Ring r ∧ i << r ⇒
    ∀x y z. x ∈ R/I ∧ y ∈ R/I ∧ z ∈ R/I ⇒ x + y + z = x + (y + z)

quotient_ring_add_comm

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R/I ∧ y ∈ R/I ⇒ x + y = y + x

quotient_ring_add_element

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R/I ∧ y ∈ R/I ⇒ x + y ∈ R/I

quotient_ring_add_group

⊢ ∀r i. Ring r ∧ i << r ⇒ Group (quotient_ring_add r i)

quotient_ring_add_id

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R/I ⇒ I + x = x

quotient_ring_add_inv

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R/I ⇒ ∃y. y ∈ R/I ∧ y + x = I

quotient_ring_by_principal_ideal

⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ Ring (r / <p>)

quotient_ring_element

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀z. z ∈ R/I ⇔ ∃x. x ∈ R ∧ z = x ∘ I

quotient_ring_has_ideal

⊢ ∀r i. Ring r ∧ i << r ⇒ I ∈ R/I

quotient_ring_homo

⊢ ∀r i. Ring r ∧ i << r ⇒ RingHomo (λx. x ∘ I) r (r / i)

quotient_ring_homo_kernel

⊢ ∀r i. Ring r ∧ i << r ⇒ kernel (λx. x ∘ I) r.sum (r / i).sum = I

quotient_ring_homo_kernel_ideal

⊢ ∀r i.
    Ring r ∧ i << r ⇒
    RingHomo (λx. x ∘ I) r (r / i) ∧ kernel_ideal (λx. x ∘ I) r (r / i) = i

quotient_ring_homo_surj

⊢ ∀r i. Ring r ∧ i << r ⇒ SURJ (λx. x ∘ I) R R/I

quotient_ring_mult_abelian_monoid

⊢ ∀r. Ring r ∧ i << r ⇒ AbelianMonoid (quotient_ring_mult r i)

quotient_ring_mult_assoc

⊢ ∀r i.
    Ring r ∧ i << r ⇒
    ∀x y z. x ∈ R/I ∧ y ∈ R/I ∧ z ∈ R/I ⇒ x * y * z = x * (y * z)

quotient_ring_mult_comm

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R/I ∧ y ∈ R/I ⇒ x * y = y * x

quotient_ring_mult_element

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x y. x ∈ R/I ∧ y ∈ R/I ⇒ x * y ∈ R/I

quotient_ring_mult_id

⊢ ∀r i. Ring r ∧ i << r ⇒ ∀x. x ∈ R/I ⇒ #1 ∘ I * x = x ∧ x * #1 ∘ I = x

quotient_ring_mult_ladd

⊢ ∀r i.
    Ring r ∧ i << r ⇒
    ∀x y z. x ∈ R/I ∧ y ∈ R/I ∧ z ∈ R/I ⇒ x * (y + z) = x * y + x * z

quotient_ring_mult_monoid

⊢ ∀r i. Ring r ∧ i << r ⇒ Monoid (quotient_ring_mult r i)

quotient_ring_property

⊢ ∀r i.
    (r / i).carrier = R/I ∧ (r / i).sum = quotient_ring_add r i ∧
    (r / i).prod = quotient_ring_mult r i

quotient_ring_ring

⊢ ∀r i. Ring r ∧ i << r ⇒ Ring (r / i)

quotient_ring_ring_sing

⊢ ∀r. Ring r ⇒ (r / r).carrier = {R}

ring_11

⊢ ∀a0 a1 a2 a0' a1' a2'.
    ring a0 a1 a2 = ring a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'

ring_Axiom

⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (ring a0 a1 a2) = f a0 a1 a2

ring_accessors

⊢ (∀f m m0. (ring f m m0).carrier = f) ∧ (∀f m m0. (ring f m m0).sum = m) ∧
  ∀f m m0. (ring f m m0).prod = m0

ring_accfupds

⊢ (∀r f. (r with sum updated_by f).carrier = R) ∧
  (∀r f. (r with prod updated_by f).carrier = R) ∧
  (∀r f. (r with carrier updated_by f).sum = r.sum) ∧
  (∀r f. (r with prod updated_by f).sum = r.sum) ∧
  (∀r f. (r with carrier updated_by f).prod = r.prod) ∧
  (∀r f. (r with sum updated_by f).prod = r.prod) ∧
  (∀r f. (r with carrier updated_by f).carrier = f R) ∧
  (∀r f. (r with sum updated_by f).sum = f r.sum) ∧
  ∀r f. (r with prod updated_by f).prod = f r.prod

ring_add_abelian_group

⊢ ∀r. Ring r ⇒ AbelianGroup r.sum

ring_add_assoc

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x + y + z = x + (y + z)

ring_add_assoc_comm

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x + (y + z) = y + (x + z)

ring_add_char_2

⊢ ∀r. Ring r ∧ char r = 2 ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + y = x − y

ring_add_comm

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + y = y + x

ring_add_element

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + y ∈ R

ring_add_eq_zero

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (x + y = #0 ⇔ y = -x)

ring_add_exp_eqn

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. r.sum.exp x n = x * ##n

ring_add_group

⊢ ∀r. Ring r ⇒
      Group r.sum ∧ r.sum.carrier = R ∧ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + y = y + x

ring_add_group_rwt

⊢ ∀r. Ring r ⇒ Group r.sum ∧ r.sum.carrier = R

ring_add_lcancel

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (x + y = x + z ⇔ y = z)

ring_add_lneg

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ -x + x = #0

ring_add_lneg_assoc

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ y = x + (-x + y) ∧ y = -x + (x + y)

ring_add_lzero

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ #0 + x = x

ring_add_pair_sub

⊢ ∀r. Ring r ⇒
      ∀x y p q.
        x ∈ R ∧ y ∈ R ∧ p ∈ R ∧ q ∈ R ⇒ x + y − (p + q) = x − p + (y − q)

ring_add_rcancel

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (y + x = z + x ⇔ y = z)

ring_add_rneg

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x + -x = #0

ring_add_rneg_assoc

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ y = y + -x + x ∧ y = y + x + -x

ring_add_rzero

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x + #0 = x

ring_add_sub

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + y − y = x

ring_add_sub_assoc

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x + y − z = x + (y − z)

ring_add_sub_comm

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ y + x − y = x

ring_add_sub_identity

⊢ ∀r. Ring r ⇒
      ∀x y z t.
        x ∈ R ∧ y ∈ R ∧ z ∈ R ∧ t ∈ R ⇒ (x + y = z + t ⇔ x − z = t − y)

ring_add_zero_zero

⊢ ∀r. Ring r ⇒ #0 + #0 = #0

ring_associates_divides

⊢ ∀r p q x. Ring r ∧ rassoc p q ∧ q ∈ R ∧ p rdivides x ⇒ q rdivides x

ring_associates_mult

⊢ ∀r p q x.
    Ring r ∧ p ∈ R ∧ q ∈ R ∧ x ∈ R ∧ rassoc p q ⇒ rassoc (x * p) (x * q)

ring_associates_refl

⊢ ∀r x. Ring r ∧ x ∈ R ⇒ rassoc x x

ring_associates_sym

⊢ ∀r p q. Ring r ∧ q ∈ R ∧ rassoc p q ⇒ rassoc q p

ring_associates_trans

⊢ ∀r x y z. Ring r ∧ z ∈ R ∧ rassoc x y ∧ rassoc y z ⇒ rassoc x z

ring_auto_I

⊢ ∀r. RingAuto I r

ring_auto_bij

⊢ ∀r f. Ring r ∧ RingAuto f r ⇒ f PERMUTES R

ring_auto_cong

⊢ ∀r f1 f2.
    Ring r ∧ (∀x. x ∈ R ⇒ f1 x = f2 x) ⇒ (RingAuto f1 r ⇔ RingAuto f2 r)

ring_auto_element

⊢ ∀r f. RingAuto f r ⇒ ∀x. x ∈ R ⇒ f x ∈ R

ring_auto_ids

⊢ ∀r f. Ring r ∧ RingAuto f r ⇒ f #0 = #0 ∧ f #1 = #1

ring_auto_linv_auto

⊢ ∀r f. Ring r ∧ RingAuto f r ⇒ RingAuto (LINV f R) r

ring_auto_one

⊢ ∀r f. Ring r ∧ RingAuto f r ⇒ f #1 = #1

ring_auto_zero

⊢ ∀r f. Ring r ∧ RingAuto f r ⇒ f #0 = #0

ring_binomial_2

⊢ ∀r. Ring r ⇒
      ∀x y. x ∈ R ∧ y ∈ R ⇒ (x + y) ** 2 = x ** 2 + ##2 * (x * y) + y ** 2

ring_binomial_3

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        (x + y) ** 3 =
        x ** 3 + ##3 * (x ** 2 * y) + ##3 * (x * y ** 2) + y ** 3

ring_binomial_4

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        (x + y) ** 4 =
        x ** 4 + ##4 * (x ** 3 * y) + ##6 * (x ** 2 * y ** 2) +
        ##4 * (x * y ** 3) + y ** 4

ring_binomial_genlist_index_shift

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀n. GENLIST
              ((λk. ##(binomial n k) * x ** SUC (n − k) * y ** k) ∘ SUC) n =
            GENLIST
              (λk. ##(binomial n (SUC k)) * x ** (n − k) * y ** SUC k) n

ring_binomial_index_shift

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀n. (λk. ##(binomial (SUC n) k) * x ** (SUC n − k) * y ** k) ∘ SUC =
            (λk. ##(binomial (SUC n) (SUC k)) * x ** (n − k) * y ** SUC k)

ring_binomial_term_merge_x

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀n. (λk. x * k) ∘ (λk. ##(binomial n k) * x ** (n − k) * y ** k) =
            (λk. ##(binomial n k) * x ** SUC (n − k) * y ** k)

ring_binomial_term_merge_y

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀n. (λk. y * k) ∘ (λk. ##(binomial n k) * x ** (n − k) * y ** k) =
            (λk. ##(binomial n k) * x ** (n − k) * y ** SUC k)

ring_binomial_thm

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀n. (x + y) ** n =
            rsum
              (GENLIST (λk. ##(binomial n k) * x ** (n − k) * y ** k)
                 (SUC n))

ring_carrier_nonempty

⊢ ∀r. Ring r ⇒ R ≠ ∅

ring_carriers

⊢ ∀r. Ring r ⇒ r.sum.carrier = R ∧ r.prod.carrier = R

ring_case_cong

⊢ ∀M M' f.
    M = M' ∧ (∀a0 a1 a2. M' = ring a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
    ring_CASE M f = ring_CASE M' f'

ring_case_eq

⊢ ring_CASE x f = v ⇔ ∃f' m m0. x = ring f' m m0 ∧ f f' m m0 = v

ring_char_0

⊢ ∀r. Ring r ∧ char r = 0 ⇒ INFINITE R

ring_char_1

⊢ ∀r. Ring r ∧ char r = 1 ⇒ R = {#0}

ring_char_2_double

⊢ ∀r. Ring r ∧ char r = 2 ⇒ ∀x. x ∈ R ⇒ x + x = #0

ring_char_2_neg_one

⊢ ∀r. Ring r ∧ char r = 2 ⇒ -#1 = #1

ring_char_2_property

⊢ ∀r. Ring r ∧ char r = 2 ⇒ #1 + #1 = #0

ring_char_alt

⊢ ∀r. Ring r ⇒
      ∀n. 0 < n ⇒ (char r = n ⇔ ##n = #0 ∧ ∀m. 0 < m ∧ m < n ⇒ ##m ≠ #0)

ring_char_divides

⊢ ∀r. Ring r ⇒ ∀n. ##n = #0 ⇔ char r divides n

ring_char_eq_1

⊢ ∀r. Ring r ⇒ (char r = 1 ⇔ #1 = #0)

ring_char_prime

⊢ ∀r. Ring r ⇒
      (prime (char r) ⇔
       1 < char r ∧ ∀k. 0 < k ∧ k < char r ⇒ ##(binomial (char r) k) = #0)

ring_char_prime_endo

⊢ ∀r. Ring r ∧ prime (char r) ⇒ RingEndo (λx. x ** char r) r

ring_component_equality

⊢ ∀r1 r2.
    r1 = r2 ⇔ r1.carrier = r2.carrier ∧ r1.sum = r2.sum ∧ r1.prod = r2.prod

ring_divides_associates

⊢ ∀r x y p.
    Ring r ∧ rassoc x y ∧ p ∈ R ∧ y ∈ R ∧ p rdivides x ⇒ p rdivides y

ring_divides_by_one

⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ #1 rdivides p

ring_divides_by_unit

⊢ ∀r. Ring r ⇒ ∀p t. p ∈ R ∧ unit t ⇒ t rdivides p

ring_divides_iso

⊢ ∀r r_ f.
    (r =r= r_) f ⇒ ∀p q. p ∈ R ∧ p rdivides q ⇒ ring_divides r_ (f p) (f q)

ring_divides_le

⊢ ∀r f.
    EuclideanRing r f ∧ ring_ordering r f ⇒
    ∀p q. p ∈ R ∧ q ∈ R ∧ p ≠ #0 ∧ q rdivides p ⇒ f q ≤ f p

ring_divides_refl

⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ p rdivides p

ring_divides_trans

⊢ ∀r. Ring r ⇒
      ∀p q t.
        p ∈ R ∧ q ∈ R ∧ t ∈ R ∧ p rdivides q ∧ q rdivides t ⇒ p rdivides t

ring_divides_zero

⊢ ∀r. Ring r ⇒ ∀p. p ∈ R ⇒ p rdivides #0

ring_eq_unit_eq

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ∧ x = y ⇒ x =~ y

ring_exp_0

⊢ ∀x. x ** 0 = #1

ring_exp_1

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x ** 1 = x

ring_exp_SUC

⊢ ∀x n. x ** SUC n = x * x ** n

ring_exp_add

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n k. x ** (n + k) = x ** n * x ** k

ring_exp_add_assoc

⊢ ∀r. Ring r ⇒
      ∀x y. x ∈ R ∧ y ∈ R ⇒ ∀n k. x ** n * (x ** k * y) = x ** (n + k) * y

ring_exp_comm

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. x ** n * x = x * x ** n

ring_exp_element

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. x ** n ∈ R

ring_exp_mod_order

⊢ ∀r. Ring r ⇒
      ∀x. x ∈ R ∧ 0 < order r.prod x ⇒
          ∀n. x ** n = x ** (n MOD order r.prod x)

ring_exp_mult

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n k. x ** (n * k) = (x ** n) ** k

ring_exp_mult_comm

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀m n. (x ** m) ** n = (x ** n) ** m

ring_exp_neg

⊢ ∀r. Ring r ⇒
      ∀x. x ∈ R ⇒ ∀n. -x ** n = if EVEN n then x ** n else -(x ** n)

ring_exp_small

⊢ ∀r. Ring r ⇒
      ∀x. x ∈ R ⇒
          x ** 0 = #1 ∧ x ** 1 = x ∧ x ** 2 = x * x ∧ x ** 3 = x * x ** 2 ∧
          x ** 4 = x * x ** 3 ∧ x ** 5 = x * x ** 4 ∧ x ** 6 = x * x ** 5 ∧
          x ** 7 = x * x ** 6 ∧ x ** 8 = x * x ** 7 ∧ x ** 9 = x * x ** 8

ring_exp_suc

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. x ** SUC n = x ** n * x

ring_factor_multiple

⊢ ∀r. Ring r ⇒
      ∀p q.
        p ∈ R ∧ q ∈ R ∧ (∃k. k ∈ R ∧ p = k * q) ⇒
        ∀z. z ∈ R ∧ (∃s. s ∈ R ∧ z = s * p) ⇒ ∃t. t ∈ R ∧ z = t * q

ring_fermat_all

⊢ ∀r. Ring r ∧ prime (char r) ⇒ ∀n k. ##n ** char r ** k = ##n

ring_fermat_thm

⊢ ∀r. Ring r ∧ prime (char r) ⇒ ∀n. ##n ** char r = ##n

ring_first_isomorphism_thm

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒
    (let
       i = kernel_ideal f r r_
     in
       i << r ∧ ring_homo_image f r r_ ≤ r_ ∧
       RingIso (f ∘ gen) (r / i) (ring_homo_image f r r_))

ring_fn_updates

⊢ (∀f0 f m m0. ring f m m0 with carrier updated_by f0 = ring (f0 f) m m0) ∧
  (∀f0 f m m0. ring f m m0 with sum updated_by f0 = ring f (f0 m) m0) ∧
  ∀f0 f m m0. ring f m m0 with prod updated_by f0 = ring f m (f0 m0)

ring_freshman_all

⊢ ∀r. Ring r ∧ prime (char r) ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀n. (x + y) ** char r ** n = x ** char r ** n + y ** char r ** n

ring_freshman_all_sub

⊢ ∀r. Ring r ∧ prime (char r) ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀n. (x − y) ** char r ** n = x ** char r ** n − y ** char r ** n

ring_freshman_thm

⊢ ∀r. Ring r ∧ prime (char r) ⇒
      ∀x y. x ∈ R ∧ y ∈ R ⇒ (x + y) ** char r = x ** char r + y ** char r

ring_freshman_thm_sub

⊢ ∀r. Ring r ∧ prime (char r) ⇒
      ∀x y. x ∈ R ∧ y ∈ R ⇒ (x − y) ** char r = x ** char r − y ** char r

ring_fun_add

⊢ ∀r. Ring r ⇒ ∀a b. rfun a ∧ rfun b ⇒ rfun (λk. a k + b k)

ring_fun_from_ring_fun

⊢ ∀r. Ring r ⇒ ∀f. rfun f ⇒ ∀x. x ∈ R ⇒ rfun (λj. f j * x ** j)

ring_fun_from_ring_fun_exp

⊢ ∀r. Ring r ⇒ ∀f. rfun f ⇒ ∀x. x ∈ R ⇒ ∀n. rfun (λj. (f j * x ** j) ** n)

ring_fun_genlist

⊢ ∀f. rfun f ⇒ ∀n. rlist (GENLIST f n)

ring_fun_map

⊢ ∀f l. rfun f ⇒ rlist (MAP f l)

ring_fupdcanon

⊢ (∀r g f.
     r with <|sum updated_by f; carrier updated_by g|> =
     r with <|carrier updated_by g; sum updated_by f|>) ∧
  (∀r g f.
     r with <|prod updated_by f; carrier updated_by g|> =
     r with <|carrier updated_by g; prod updated_by f|>) ∧
  ∀r g f.
    r with <|prod updated_by f; sum updated_by g|> =
    r with <|sum updated_by g; prod updated_by f|>

ring_fupdcanon_comp

⊢ ((∀g f. sum_fupd f ∘ carrier_fupd g = carrier_fupd g ∘ sum_fupd f) ∧
   ∀h g f.
     sum_fupd f ∘ carrier_fupd g ∘ h = carrier_fupd g ∘ sum_fupd f ∘ h) ∧
  ((∀g f. prod_fupd f ∘ carrier_fupd g = carrier_fupd g ∘ prod_fupd f) ∧
   ∀h g f.
     prod_fupd f ∘ carrier_fupd g ∘ h = carrier_fupd g ∘ prod_fupd f ∘ h) ∧
  (∀g f. prod_fupd f ∘ sum_fupd g = sum_fupd g ∘ prod_fupd f) ∧
  ∀h g f. prod_fupd f ∘ sum_fupd g ∘ h = sum_fupd g ∘ prod_fupd f ∘ h

ring_fupdfupds

⊢ (∀r g f.
     r with <|carrier updated_by f; carrier updated_by g|> =
     r with carrier updated_by f ∘ g) ∧
  (∀r g f.
     r with <|sum updated_by f; sum updated_by g|> =
     r with sum updated_by f ∘ g) ∧
  ∀r g f.
    r with <|prod updated_by f; prod updated_by g|> =
    r with prod updated_by f ∘ g

ring_fupdfupds_comp

⊢ ((∀g f. carrier_fupd f ∘ carrier_fupd g = carrier_fupd (f ∘ g)) ∧
   ∀h g f. carrier_fupd f ∘ carrier_fupd g ∘ h = carrier_fupd (f ∘ g) ∘ h) ∧
  ((∀g f. sum_fupd f ∘ sum_fupd g = sum_fupd (f ∘ g)) ∧
   ∀h g f. sum_fupd f ∘ sum_fupd g ∘ h = sum_fupd (f ∘ g) ∘ h) ∧
  (∀g f. prod_fupd f ∘ prod_fupd g = prod_fupd (f ∘ g)) ∧
  ∀h g f. prod_fupd f ∘ prod_fupd g ∘ h = prod_fupd (f ∘ g) ∘ h

ring_gcd_divides

⊢ ∀r f.
    EuclideanRing r f ⇒
    ∀p q. p ∈ R ∧ q ∈ R ⇒ rgcd p q rdivides p ∧ rgcd p q rdivides q

ring_gcd_element

⊢ ∀r f. EuclideanRing r f ⇒ ∀p q. p ∈ R ∧ q ∈ R ⇒ rgcd p q ∈ R

ring_gcd_is_gcd

⊢ ∀r f.
    EuclideanRing r f ⇒
    ∀p q.
      p ∈ R ∧ q ∈ R ⇒
      rgcd p q rdivides p ∧ rgcd p q rdivides q ∧
      ∀d. d ∈ R ∧ d rdivides p ∧ d rdivides q ⇒ d rdivides rgcd p q

ring_gcd_linear

⊢ ∀r f.
    EuclideanRing r f ⇒
    ∀p q. p ∈ R ∧ q ∈ R ⇒ ∃a b. a ∈ R ∧ b ∈ R ∧ rgcd p q = a * p + b * q

ring_gcd_property

⊢ ∀r f.
    EuclideanRing r f ⇒
    ∀p q.
      p ∈ R ∧ q ∈ R ⇒
      ∀d. d ∈ R ∧ d rdivides p ∧ d rdivides q ⇒ d rdivides rgcd p q

ring_gcd_sym

⊢ ∀r f. EuclideanRing r f ⇒ ∀p q. p ∈ R ∧ q ∈ R ⇒ rgcd p q = rgcd q p

ring_gcd_zero

⊢ ∀r f p. rgcd p #0 = p ∧ rgcd #0 p = p

ring_homo_I_refl

⊢ ∀r. RingHomo I r r

ring_homo_add

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x + y) = f x +_ f y

ring_homo_char_divides

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ char r_ divides char r

ring_homo_compose

⊢ ∀r s t f1 f2. RingHomo f1 r s ∧ RingHomo f2 s t ⇒ RingHomo (f2 ∘ f1) r t

ring_homo_cong

⊢ ∀r r_ f1 f2.
    Ring r ∧ Ring r_ ∧ (∀x. x ∈ R ⇒ f1 x = f2 x) ⇒
    (RingHomo f1 r r_ ⇔ RingHomo f2 r r_)

ring_homo_element

⊢ ∀r r_ f. RingHomo f r r_ ⇒ ∀x. x ∈ R ⇒ f x ∈ R_

ring_homo_eq_zero

⊢ ∀r r_ f. (r ~r~ r_) f ∧ INJ f R R_ ⇒ ∀x. x ∈ R ⇒ (f x = #0_ ⇔ x = #0)

ring_homo_exp

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. x ∈ R ⇒ ∀n. f (x ** n) = f x **_ n

ring_homo_ideal_group

⊢ ∀r s f. (r ~r~ s) f ⇒ ∀i. i << r ⇒ Group (homo_ideal f r s i).sum

ring_homo_ideal_ideal

⊢ ∀r s f.
    Ring r ∧ Ring s ∧ RingHomo f r s ∧ SURJ f R s.carrier ⇒
    ∀i. i << r ⇒ homo_ideal f r s i << s

ring_homo_ideal_subgroup

⊢ ∀r s f. (r ~r~ s) f ⇒ ∀i. i << r ⇒ (homo_ideal f r s i).sum ≤ s.sum

ring_homo_ids

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ f #0 = #0_ ∧ f #1 = #1_

ring_homo_image_bij

⊢ ∀r r_ f.
    (r ~r~ r_) f ∧ INJ f R R_ ⇒ BIJ f R (ring_homo_image f r r_).carrier

ring_homo_image_carrier

⊢ ∀r r_ f. (ring_homo_image f r r_).carrier = IMAGE f R

ring_homo_image_homo

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ RingHomo f r (ring_homo_image f r r_)

ring_homo_image_is_subring

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ subring (ring_homo_image f r r_) r_

ring_homo_image_iso

⊢ ∀r r_ f. (r ~r~ r_) f ∧ INJ f R R_ ⇒ RingIso f r (ring_homo_image f r r_)

ring_homo_image_ring

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ Ring (ring_homo_image f r r_)

ring_homo_image_subring

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ring_homo_image f r r_ ≤ r_

ring_homo_image_subring_subring

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒
    ∀s. Ring s ∧ subring s r ⇒ subring (ring_homo_image f s r_) r_

ring_homo_image_surj_property

⊢ ∀r r_ f.
    Ring r ∧ Ring r_ ∧ SURJ f R R_ ⇒ RingIso I r_ (ring_homo_image f r r_)

ring_homo_inv

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. unit x ⇒ f ( |/ x) = |/_ (f x)

ring_homo_kernel_ideal

⊢ ∀f r s. (r ~r~ s) f ⇒ kernel_ideal f r s << r

ring_homo_linv_homo

⊢ ∀r r_ f. (r ~r~ r_) f ∧ BIJ f R R_ ⇒ RingHomo (LINV f R) r_ r

ring_homo_mult

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x * y) = f x *_ f y

ring_homo_neg

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. x ∈ R ⇒ f (-x) = $-_ (f x)

ring_homo_num

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀n. f (##n) = ##_ #1_ n

ring_homo_num_nonzero

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒ ∀c. 0 < c ∧ c < char r_ ⇒ ##c ≠ #0 ∧ f (##c) ≠ #0_

ring_homo_one

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ f #1 = #1_

ring_homo_one_eq_zero

⊢ ∀r r_ f. (r ~r~ r_) f ∧ #1 = #0 ⇒ #1_ = #0_

ring_homo_property

⊢ ∀r r_ f.
    Ring r ∧ RingHomo f r r_ ⇒
    ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x + y) = f x +_ f y ∧ f (x * y) = f x *_ f y

ring_homo_ring_homo_subring

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ subring (ring_homo_image f r r_) r_

ring_homo_sub

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x − y) = f x -_ f y

ring_homo_subring_homo

⊢ ∀r s r_ f. (r ~r~ r_) f ∧ s ≤ r ⇒ (s ~r~ ring_homo_image f s r_) f

ring_homo_sum_num_property

⊢ ∀r r_ f.
    (r ~r~ r_) f ⇒ ∀c. 0 < c ∧ c < char r_ ⇒ ##c ≠ #0 ∧ ##_ #1_ c ≠ #0_

ring_homo_sym

⊢ ∀r r_ f. (r ~r~ r_) f ∧ BIJ f R R_ ⇒ RingHomo (LINV f R) r_ r

ring_homo_sym_any

⊢ Ring r ∧ Ring s ∧ RingHomo f r s ∧
  (∀x. x ∈ s.carrier ⇒ i x ∈ R ∧ f (i x) = x) ∧ (∀x. x ∈ R ⇒ i (f x) = x) ⇒
  RingHomo i s r

ring_homo_trans

⊢ ∀r s t f1 f2. RingHomo f1 r s ∧ RingHomo f2 s t ⇒ RingHomo (f2 ∘ f1) r t

ring_homo_unit

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. unit x ⇒ unit_ (f x)

ring_homo_unit_inv

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. unit x ⇒ |/_ (f x) = f ( |/ x)

ring_homo_unit_inv_element

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ ∀x. unit x ⇒ |/_ (f x) ∈ R_

ring_homo_unit_inv_nonzero

⊢ ∀r r_ f. (r ~r~ r_) f ∧ #1_ ≠ #0_ ⇒ ∀x. unit x ⇒ |/_ (f x) ≠ #0_

ring_homo_unit_nonzero

⊢ ∀r r_ f. (r ~r~ r_) f ∧ #1_ ≠ #0_ ⇒ ∀x. unit x ⇒ f x ≠ #0_

ring_homo_zero

⊢ ∀r r_ f. (r ~r~ r_) f ⇒ f #0 = #0_

ring_induction

⊢ ∀P. (∀f m m0. P (ring f m m0)) ⇒ ∀r. P r

ring_inj_image_alt

⊢ ∀r f.
    Ring r ⇒
    ring_inj_image r f =
    <|carrier := IMAGE f R; sum := monoid_inj_image r.sum f;
      prod := monoid_inj_image r.prod f|>

ring_inj_image_carrier

⊢ ∀r f. (ring_inj_image r f).carrier = IMAGE f R

ring_inj_image_prod_abelian_monoid

⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ AbelianMonoid (ring_inj_image r f).prod

ring_inj_image_prod_monoid

⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ Monoid (ring_inj_image r f).prod

ring_inj_image_prod_monoid_homo

⊢ ∀r f.
    Ring r ∧ INJ f R 𝕌(:β) ⇒ MonoidHomo f r.prod (ring_inj_image r f).prod

ring_inj_image_ring

⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ Ring (ring_inj_image r f)

ring_inj_image_ring_homo

⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ RingHomo f r (ring_inj_image r f)

ring_inj_image_sum_abelian_group

⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ AbelianGroup (ring_inj_image r f).sum

ring_inj_image_sum_group

⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ Group (ring_inj_image r f).sum

ring_inj_image_sum_group_homo

⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ GroupHomo f r.sum (ring_inj_image r f).sum

ring_inj_image_sum_monoid

⊢ ∀r f. Ring r ∧ INJ f R 𝕌(:β) ⇒ Monoid (ring_inj_image r f).sum

ring_inv_one

⊢ ∀r. Ring r ⇒ |/ #1 = #1

ring_irreducible_gcd

⊢ ∀r f.
    EuclideanRing r f ⇒
    ∀p. p ∈ R ∧ atom p ⇒ ∀q. q ∈ R ⇒ unit (rgcd p q) ∨ p rdivides q

ring_iso_I_refl

⊢ ∀r. RingIso I r r

ring_iso_add

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x + y) = f x +_ f y

ring_iso_bij

⊢ ∀r r_ f. (r =r= r_) f ⇒ BIJ f R R_

ring_iso_card_eq

⊢ ∀r r_ f. RingIso f r r_ ∧ FINITE R ⇒ CARD R = CARD R_

ring_iso_char_eq

⊢ ∀r r_ f. (r =r= r_) f ⇒ char r_ = char r

ring_iso_compose

⊢ ∀r s t f1 f2. RingIso f1 r s ∧ RingIso f2 s t ⇒ RingIso (f2 ∘ f1) r t

ring_iso_cong

⊢ ∀r r_ f1 f2.
    Ring r ∧ Ring r_ ∧ (∀x. x ∈ R ⇒ f1 x = f2 x) ⇒
    (RingIso f1 r r_ ⇔ RingIso f2 r r_)

ring_iso_element

⊢ ∀r r_ f. RingIso f r r_ ⇒ ∀x. x ∈ R ⇒ f x ∈ R_

ring_iso_element_unique

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (f x = f y ⇔ x = y)

ring_iso_eq_one

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. x ∈ R ⇒ (f x = #1_ ⇔ x = #1)

ring_iso_eq_zero

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. x ∈ R ⇒ (f x = #0_ ⇔ x = #0)

ring_iso_exp

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. x ∈ R ⇒ ∀n. f (x ** n) = f x **_ n

ring_iso_ids

⊢ ∀r r_ f. (r =r= r_) f ⇒ f #0 = #0_ ∧ f #1 = #1_

ring_iso_inv

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. unit x ⇒ f ( |/ x) = |/_ (f x)

ring_iso_inverse

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀y. y ∈ R_ ⇒ ∃x. x ∈ R ∧ y = f x

ring_iso_inverse_element

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀y. y ∈ R_ ⇒ LINV f R y ∈ R ∧ y = f (LINV f R y)

ring_iso_linv_iso

⊢ ∀r r_ f. (r =r= r_) f ⇒ RingIso (LINV f R) r_ r

ring_iso_mult

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x * y) = f x *_ f y

ring_iso_neg

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. x ∈ R ⇒ f (-x) = $-_ (f x)

ring_iso_nonzero

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. x ∈ R+ ⇒ f x ∈ R+_

ring_iso_num

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀n. f (##n) = ##_ #1_ n

ring_iso_one

⊢ ∀r r_ f. (r =r= r_) f ⇒ f #1 = #1_

ring_iso_property

⊢ ∀r r_ f.
    Ring r ∧ RingIso f r r_ ⇒
    ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x + y) = f x +_ f y ∧ f (x * y) = f x *_ f y

ring_iso_ring_homo_subring

⊢ ∀r r_ f. (r =r= r_) f ⇒ subring (ring_homo_image f r r_) r_

ring_iso_sub

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ f (x − y) = f x -_ f y

ring_iso_subring_iso

⊢ ∀r s r_ f. (r =r= r_) f ∧ s ≤ r ⇒ (s =r= ring_homo_image f s r_) f

ring_iso_sym

⊢ ∀r r_ f. (r =r= r_) f ⇒ RingIso (LINV f R) r_ r

ring_iso_sym_any

⊢ Ring r ∧ Ring s ∧ RingIso f r s ∧
  (∀x. x ∈ s.carrier ⇒ i x ∈ R ∧ f (i x) = x) ∧ (∀x. x ∈ R ⇒ i (f x) = x) ⇒
  RingIso i s r

ring_iso_trans

⊢ ∀r s t f1 f2. RingIso f1 r s ∧ RingIso f2 s t ⇒ RingIso (f2 ∘ f1) r t

ring_iso_unit

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀x. unit x ⇒ unit_ (f x)

ring_iso_zero

⊢ ∀r r_ f. (r =r= r_) f ⇒ f #0 = #0_

ring_list_SNOC

⊢ ∀x s. rlist (SNOC x s) ⇔ x ∈ R ∧ rlist s

ring_list_cons

⊢ ∀r h t. rlist (h::t) ⇔ h ∈ R ∧ rlist t

ring_list_from_genlist

⊢ ∀r f. rfun f ⇒ ∀n. rlist (GENLIST f n)

ring_list_from_genlist_ring_fun

⊢ ∀r f. rfun f ⇒ ∀n g. rlist (GENLIST (f ∘ g) n)

ring_list_front_last

⊢ ∀s. rlist (FRONT s) ∧ LAST s ∈ R ⇒ rlist s

ring_list_gen_from_ring_fun

⊢ ∀r. Ring r ⇒
      ∀f. rfun f ⇒ ∀x. x ∈ R ⇒ ∀n. rlist (GENLIST (λj. f j * x ** j) n)

ring_list_nil

⊢ ∀r. rlist [] ⇔ T

ring_literal_11

⊢ ∀f1 m01 m1 f2 m02 m2.
    <|carrier := f1; sum := m01; prod := m1|> =
    <|carrier := f2; sum := m02; prod := m2|> ⇔
    f1 = f2 ∧ m01 = m02 ∧ m1 = m2

ring_literal_nchotomy

⊢ ∀r. ∃f m0 m. r = <|carrier := f; sum := m0; prod := m|>

ring_mult_abelian_monoid

⊢ ∀r. Ring r ⇒ AbelianMonoid r.prod

ring_mult_add

⊢ ∀r. Ring r ⇒
      ∀z y x.
        x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒
        x * (y + z) = x * y + x * z ∧ (y + z) * x = y * x + z * x

ring_mult_add_neg

⊢ ∀r. Ring r ⇒
      ∀x. x ∈ R ⇒ ∀n. ##n * x + -x = if n = 0 then -x else ##(n − 1) * x

ring_mult_add_neg_assoc

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀n. ##n * x + (-x + y) =
            if n = 0 then -x + y else ##(n − 1) * x + y

ring_mult_add_neg_mult

⊢ ∀r. Ring r ⇒
      ∀x. x ∈ R ⇒
          ∀m n.
            ##m * x + -(##n * x) =
            if m < n then -(##(n − m) * x) else ##(m − n) * x

ring_mult_add_neg_mult_assoc

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀m n.
          ##m * x + (-(##n * x) + y) =
          if m < n then -(##(n − m) * x) + y else ##(m − n) * x + y

ring_mult_assoc

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * y * z = x * (y * z)

ring_mult_assoc_comm

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * (y * z) = y * (x * z)

ring_mult_comm

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x * y = y * x

ring_mult_divides

⊢ ∀r p q x.
    Ring r ∧ p * q rdivides x ∧ p ∈ R ∧ q ∈ R ⇒ p rdivides x ∧ q rdivides x

ring_mult_element

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x * y ∈ R

ring_mult_exp

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ ∀n. (x * y) ** n = x ** n * y ** n

ring_mult_ladd

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (y + z) * x = y * x + z * x

ring_mult_lneg

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -x * y = -(x * y)

ring_mult_lone

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ #1 * x = x

ring_mult_lsub

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * z − y * z = (x − y) * z

ring_mult_lzero

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ #0 * x = #0

ring_mult_monoid

⊢ ∀r. Ring r ⇒
      Monoid r.prod ∧ r.prod.carrier = R ∧
      ∀x y. x ∈ R ∧ y ∈ R ⇒ x * y = y * x

ring_mult_monoid_rwt

⊢ ∀r. Ring r ⇒ Monoid r.prod ∧ r.prod.carrier = R

ring_mult_neg_neg

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -x * -y = x * y

ring_mult_one_one

⊢ ∀r. Ring r ⇒ #1 * #1 = #1

ring_mult_pair_diff

⊢ ∀r. Ring r ⇒
      ∀x y p q.
        x ∈ R ∧ y ∈ R ∧ p ∈ R ∧ q ∈ R ⇒
        x * y − p * q = (x − p) * y + p * (y − q)

ring_mult_pair_sub

⊢ ∀r. Ring r ⇒
      ∀x y p q.
        x ∈ R ∧ y ∈ R ∧ p ∈ R ∧ q ∈ R ⇒
        x * y − p * q = (x − p) * (y − q) + (x − p) * q + p * (y − q)

ring_mult_radd

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * (y + z) = x * y + x * z

ring_mult_rneg

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x * -y = -(x * y)

ring_mult_rone

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x * #1 = x

ring_mult_rsub

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x * y − x * z = x * (y − z)

ring_mult_rzero

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x * #0 = #0

ring_mult_zero_zero

⊢ ∀r. Ring r ⇒ #0 * #0 = #0

ring_nchotomy

⊢ ∀rr. ∃f m m0. rr = ring f m m0

ring_neg_add

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -(x + y) = -x + -y

ring_neg_add_comm

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -(x + y) = -y + -x

ring_neg_add_neg

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ -x + -x = -(##2 * x)

ring_neg_add_neg_assoc

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -x + (-x + y) = -(##2 * x) + y

ring_neg_add_neg_mult

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. -x + -(##n * x) = -(##(n + 1) * x)

ring_neg_add_neg_mult_assoc

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒ ∀n. -x + (-(##n * x) + y) = -(##(n + 1) * x) + y

ring_neg_char_2

⊢ ∀r. Ring r ∧ char r = 2 ⇒ ∀x. x ∈ R ⇒ -x = x

ring_neg_element

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ -x ∈ R

ring_neg_eq

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (-x = -y ⇔ x = y)

ring_neg_eq_swap

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (-x = y ⇔ x = -y)

ring_neg_eq_zero

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ (-x = #0 ⇔ x = #0)

ring_neg_exp

⊢ ∀r. Ring r ⇒
      ∀x. x ∈ R ⇒ ∀n. -x ** n = if EVEN n then x ** n else -(x ** n)

ring_neg_mult

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -(x * y) = -x * y ∧ -(x * y) = x * -y

ring_neg_mult_add_neg_mult

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀m n. -(##m * x) + -(##n * x) = -(##(m + n) * x)

ring_neg_mult_add_neg_mult_assoc

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀m n. -(##m * x) + (-(##n * x) + y) = -(##(m + n) * x) + y

ring_neg_neg

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ --x = x

ring_neg_nonzero

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R+ ⇒ -x ∈ R+

ring_neg_one_eq_one

⊢ ∀r. Ring r ∧ #1 ≠ #0 ⇒ (-#1 = #1 ⇔ char r = 2)

ring_neg_square

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ -x ** 2 = x ** 2

ring_neg_sub

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ -(x − y) = y − x

ring_neg_zero

⊢ ∀r. Ring r ⇒ -#0 = #0

ring_nonzero_element

⊢ ∀r x. x ∈ R+ ⇒ x ∈ R

ring_nonzero_eq

⊢ ∀r x. x ∈ R+ ⇔ x ∈ R ∧ x ≠ #0

ring_nonzero_mult_carrier

⊢ ∀r. Ring r ⇒ F* = R+

ring_num_0

⊢ ∀r. ##0 = #0

ring_num_1

⊢ ∀r. Ring r ⇒ ##1 = #1

ring_num_2

⊢ ∀r. Ring r ⇒ ##2 = #1 + #1

ring_num_SUC

⊢ ∀r. Ring r ⇒ ∀n. ##(SUC n) = #1 + ##n

ring_num_add

⊢ ∀r. Ring r ⇒ ∀n k. ##(n + k) = ##n + ##k

ring_num_add_assoc

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀m n. ##m + (##n + x) = ##(m + n) + x

ring_num_add_mult

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀m n. ##(m + n) * x = ##m * x + ##n * x

ring_num_add_mult_assoc

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒ ∀m n. ##(m + n) * x + y = ##m * x + (##n * x + y)

ring_num_all_zero

⊢ ∀r. Ring r ⇒ #1 = #0 ⇒ ∀c. ##c = #0

ring_num_char_coprime_nonzero

⊢ ∀r. Ring r ∧ #1 ≠ #0 ⇒ ∀c. coprime c (char r) ⇒ ##c ≠ #0

ring_num_element

⊢ ∀r. Ring r ⇒ ∀n. ##n ∈ R

ring_num_eq

⊢ ∀r. Ring r ⇒ ∀n m. n < char r ∧ m < char r ⇒ (##n = ##m ⇔ n = m)

ring_num_exp

⊢ ∀r. Ring r ⇒ ∀m n. ##m ** n = ##(m ** n)

ring_num_mod

⊢ ∀r. Ring r ∧ 0 < char r ⇒ ∀n. ##n = ##(n MOD char r)

ring_num_mult

⊢ ∀r. Ring r ⇒ ∀m n. ##m * ##n = ##(m * n)

ring_num_mult_assoc

⊢ ∀r. Ring r ⇒ ∀m n x. x ∈ R ⇒ ##m * (##n * x) = ##(m * n) * x

ring_num_mult_element

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. ##n * x ∈ R

ring_num_mult_exp

⊢ ∀r. Ring r ⇒ ∀k m n. ##k * ##m ** n = ##(k * m ** n)

ring_num_mult_neg

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. -(##n * x) = ##n * -x

ring_num_mult_radd

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ ∀n. ##n * (x + y) = ##n * x + ##n * y

ring_num_mult_small

⊢ ∀r. Ring r ⇒
      ∀x. x ∈ R ⇒
          #0 * x = #0 ∧ #1 * x = x ∧ ##2 * x = x + x ∧
          ##3 * x = ##2 * x + x

ring_num_mult_suc

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. ##(SUC n) * x = ##n * x + x

ring_num_negative

⊢ ∀r. Ring r ∧ 0 < char r ⇒ ∀z. ∃y x. y = ##x ∧ y + ##z = #0

ring_num_one

⊢ ∀r. ##1 = #1 + #0

ring_num_sub

⊢ ∀r. Ring r ⇒ ∀n m. m < n ⇒ ##(n − m) = ##n − ##m

ring_num_suc

⊢ ∀r. Ring r ⇒ ∀n. ##(SUC n) = ##n + #1

ring_one_element

⊢ ∀r. Ring r ⇒ #1 ∈ R

ring_one_eq_zero

⊢ ∀r. Ring r ⇒ (#1 = #0 ⇔ R = {#0})

ring_one_exp

⊢ ∀r. Ring r ⇒ ∀n. #1 ** n = #1

ring_one_unique

⊢ ∀r. Ring r ⇒ ∀y. y ∈ R ⇒ ((∀x. x ∈ R ⇒ y * x = x ∨ x * y = x) ⇔ y = #1)

ring_prime_divides_product

⊢ ∀r. Ring r ⇒
      ∀p. p ∈ R ⇒
          (rprime p ∧ p ∉ R* ⇔
           ∀b. FINITE_BAG b ∧ SET_OF_BAG b ⊆ R ∧ p rdivides GBAG r.prod b ⇒
               ∃x. x ⋲ b ∧ p rdivides x)

ring_prime_iso

⊢ ∀r r_ f. (r =r= r_) f ⇒ ∀p. p ∈ R ∧ rprime p ⇒ ring_prime r_ (f p)

ring_product_factors_divide

⊢ ∀r. Ring r ⇒
      ∀b. FINITE_BAG b ⇒
          SET_OF_BAG b ⊆ R ∧ GBAG r.prod b rdivides x ⇒
          ∀y. y ⋲ b ⇒ y rdivides x

ring_single_add_mult

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. x + ##n * x = ##(n + 1) * x

ring_single_add_mult_assoc

⊢ ∀r. Ring r ⇒
      ∀x y. x ∈ R ∧ y ∈ R ⇒ ∀n. x + (##n * x + y) = ##(n + 1) * x + y

ring_single_add_neg_mult

⊢ ∀r. Ring r ⇒
      ∀x. x ∈ R ⇒
          ∀n. x + -(##n * x) = if n = 0 then x else -(##(n − 1) * x)

ring_single_add_neg_mult_assoc

⊢ ∀r. Ring r ⇒
      ∀x y.
        x ∈ R ∧ y ∈ R ⇒
        ∀n. x + (-(##n * x) + y) =
            if n = 0 then x + y else -(##(n − 1) * x) + y

ring_single_add_single

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x + x = ##2 * x

ring_single_add_single_assoc

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x + (x + y) = ##2 * x + y

ring_single_mult_exp

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. x * x ** n = x ** (n + 1)

ring_single_mult_exp_assoc

⊢ ∀r. Ring r ⇒
      ∀x y. x ∈ R ∧ y ∈ R ⇒ ∀n. x * (x ** n * y) = x ** (n + 1) * y

ring_single_mult_single

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x * x = x ** 2

ring_single_mult_single_assoc

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x * (x * y) = x ** 2 * y

ring_sub_add

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x − y + y = x

ring_sub_element

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ x − y ∈ R

ring_sub_eq

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ⇒ x − x = #0

ring_sub_eq_add

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (x − y = z ⇔ x = y + z)

ring_sub_eq_zero

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (x − y = #0 ⇔ x = y)

ring_sub_lcancel

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (x − y = x − z ⇔ y = z)

ring_sub_pair_reduce

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ x + z − (y + z) = x − y

ring_sub_rcancel

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ⇒ (y − x = z − x ⇔ y = z)

ring_sub_zero

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x − #0 = x

ring_sum_SNOC

⊢ ∀r. Ring r ⇒ ∀k s. k ∈ R ∧ rlist s ⇒ rsum (SNOC k s) = rsum s + k

ring_sum_append

⊢ ∀r. Ring r ⇒ ∀s t. rlist s ∧ rlist t ⇒ rsum (s ⧺ t) = rsum s + rsum t

ring_sum_cons

⊢ ∀r h t. rsum (h::t) = h + rsum t

ring_sum_decompose_first

⊢ ∀r f n. rsum (GENLIST f (SUC n)) = f 0 + rsum (GENLIST (f ∘ SUC) n)

ring_sum_decompose_first_last

⊢ ∀r. Ring r ⇒
      ∀f n.
        rfun f ∧ 0 < n ⇒
        rsum (GENLIST f (SUC n)) =
        f 0 + rsum (GENLIST (f ∘ SUC) (PRE n)) + f n

ring_sum_decompose_last

⊢ ∀r. Ring r ⇒
      ∀f n. rfun f ⇒ rsum (GENLIST f (SUC n)) = rsum (GENLIST f n) + f n

ring_sum_element

⊢ ∀r. Ring r ⇒ ∀s. rlist s ⇒ rsum s ∈ R

ring_sum_freshman_all

⊢ ∀r. Ring r ∧ prime (char r) ⇒
      ∀f. rfun f ⇒
          ∀x. x ∈ R ⇒
              ∀n k.
                rsum (GENLIST (λj. f j * x ** j) n) ** char r ** k =
                rsum (GENLIST (λj. (f j * x ** j) ** char r ** k) n)

ring_sum_freshman_thm

⊢ ∀r. Ring r ∧ prime (char r) ⇒
      ∀f. rfun f ⇒
          ∀x. x ∈ R ⇒
              ∀n. rsum (GENLIST (λj. f j * x ** j) n) ** char r =
                  rsum (GENLIST (λj. (f j * x ** j) ** char r) n)

ring_sum_fun_zero

⊢ ∀r. Ring r ⇒
      ∀f. rfun f ⇒
          ∀n. (∀k. 0 < k ∧ k < n ⇒ f k = #0) ⇒
              rsum (MAP f (GENLIST SUC (PRE n))) = #0

ring_sum_genlist_add

⊢ ∀r. Ring r ⇒
      ∀a b.
        rfun a ∧ rfun b ⇒
        ∀n. rsum (GENLIST a n) + rsum (GENLIST b n) =
            rsum (GENLIST (λk. a k + b k) n)

ring_sum_genlist_append

⊢ ∀r. Ring r ⇒
      ∀a b.
        rfun a ∧ rfun b ⇒
        ∀n. rsum (GENLIST a n ⧺ GENLIST b n) =
            rsum (GENLIST (λk. a k + b k) n)

ring_sum_genlist_const

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ ∀n. rsum (GENLIST (K x) n) = ##n * x

ring_sum_genlist_sum

⊢ ∀r. Ring r ⇒
      ∀f. rfun f ⇒
          ∀n m.
            rsum (GENLIST f (n + m)) =
            rsum (GENLIST f m) + rsum (GENLIST (λk. f (k + m)) n)

ring_sum_mult

⊢ ∀r. Ring r ⇒
      ∀k s. k ∈ R ∧ rlist s ⇒ k * rsum s = rsum (MAP (λx. k * x) s)

ring_sum_mult_ladd

⊢ ∀r. Ring r ⇒
      ∀m n s.
        m ∈ R ∧ n ∈ R ∧ rlist s ⇒
        (m + n) * rsum s =
        rsum (MAP (λx. m * x) s) + rsum (MAP (λx. n * x) s)

ring_sum_nil

⊢ ∀r. rsum [] = #0

ring_sum_sing

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ rsum [x] = x

ring_sum_zero

⊢ ∀r. Ring r ⇒ ∀n. r.sum.exp #0 n = #0

ring_unit_element

⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ x ∈ R

ring_unit_has_inv

⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ unit ( |/ x)

ring_unit_inv_element

⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ |/ x ∈ R

ring_unit_inv_inv

⊢ ∀r. Ring r ⇒ ∀u. unit u ⇒ u = |/ ( |/ u)

ring_unit_inv_nonzero

⊢ ∀r. Ring r ∧ #1 ≠ #0 ⇒ ∀x. unit x ⇒ |/ x ≠ #0

ring_unit_linv

⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ |/ x * x = #1

ring_unit_linv_inv

⊢ ∀r. Ring r ⇒ ∀u v. unit u ∧ v ∈ R ∧ |/ u * v = #1 ⇒ u = v

ring_unit_linv_unique

⊢ ∀r. Ring r ⇒ ∀u v. u ∈ R ∧ unit v ∧ u * v = #1 ⇒ u = |/ v

ring_unit_mult_eq_unit

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ⇒ (unit (x * y) ⇔ unit x ∧ unit y)

ring_unit_mult_unit

⊢ ∀r. Ring r ⇒ ∀u v. unit u ∧ unit v ⇒ unit (u * v)

ring_unit_mult_zero

⊢ ∀r. Ring r ⇒ ∀x y. unit x ∧ y ∈ R ⇒ (x * y = #0 ⇔ y = #0)

ring_unit_neg

⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ unit (-x)

ring_unit_nonzero

⊢ ∀r. Ring r ∧ #1 ≠ #0 ⇒ ∀x. unit x ⇒ x ≠ #0

ring_unit_one

⊢ ∀r. Ring r ⇒ unit #1

ring_unit_property

⊢ ∀r. Ring r ⇒ ∀u. unit u ⇔ u ∈ R ∧ ∃v. v ∈ R ∧ u * v = #1

ring_unit_rinv

⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ x * |/ x = #1

ring_unit_rinv_inv

⊢ ∀r. Ring r ⇒ ∀u v. u ∈ R ∧ unit v ∧ u * |/ v = #1 ⇒ u = v

ring_unit_rinv_unique

⊢ ∀r. Ring r ⇒ ∀u v. unit u ∧ v ∈ R ∧ u * v = #1 ⇒ v = |/ u

ring_unit_zero

⊢ ∀r. Ring r ⇒ (unit #0 ⇔ #1 = #0)

ring_units_abelain_group

⊢ ∀r. Ring r ⇒ AbelianGroup r*

ring_units_element

⊢ ∀r. Ring r ⇒ ∀x. unit x ⇒ x ∈ R

ring_units_group

⊢ ∀r. Ring r ⇒ Group r*

ring_units_has_one

⊢ ∀r. Ring r ⇒ unit #1

ring_units_has_zero

⊢ ∀r. Ring r ⇒ (unit #0 ⇔ #1 = #0)

ring_units_property

⊢ ∀r. Ring r ⇒ r*.op = $* ∧ r*.id = #1

ring_updates_eq_literal

⊢ ∀r f m0 m.
    r with <|carrier := f; sum := m0; prod := m|> =
    <|carrier := f; sum := m0; prod := m|>

ring_zero_divides

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ (#0 rdivides x ⇔ x = #0)

ring_zero_element

⊢ ∀r. Ring r ⇒ #0 ∈ R

ring_zero_exp

⊢ ∀r. Ring r ⇒ ∀n. #0 ** n = if n = 0 then #1 else #0

ring_zero_fix

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ (x + x = x ⇔ x = #0)

ring_zero_sub

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ #0 − x = -x

ring_zero_unique

⊢ ∀r. Ring r ⇒
      ∀x y. x ∈ R ∧ y ∈ R ⇒ (y + x = x ⇔ y = #0) ∧ (x + y = x ⇔ y = #0)

subring_I_antisym

⊢ ∀r s. subring s r ∧ subring r s ⇒ RingIso I s r

subring_add

⊢ ∀r s. s ≤ r ⇒ ∀x y. x ∈ B ∧ y ∈ B ⇒ s.sum.op x y = x + y

subring_by_subgroup_submonoid

⊢ ∀r s.
    s ≤ r ⇔
    Ring r ∧ Ring s ∧ subgroup s.sum r.sum ∧ submonoid s.prod r.prod

subring_carrier_antisym

⊢ ∀r s. subring s r ∧ R ⊆ B ⇒ RingIso I s r

subring_carrier_finite

⊢ ∀r s. FiniteRing r ∧ subring s r ⇒ FINITE B

subring_carrier_subset

⊢ ∀r s. subring s r ⇒ B ⊆ R

subring_char

⊢ ∀r s. s ≤ r ⇒ char s = char r

subring_char_divides

⊢ ∀r s. s ≤ r ⇒ char r divides char s

subring_element

⊢ ∀r s. subring s r ⇒ ∀x. x ∈ B ⇒ x ∈ R

subring_element_alt

⊢ ∀r s. s ≤ r ⇒ ∀x. x ∈ B ⇒ x ∈ R

subring_exp

⊢ ∀r s. s ≤ r ⇒ ∀x. x ∈ B ⇒ ∀n. s.prod.exp x n = x ** n

subring_finite_ring

⊢ ∀r s. FiniteRing r ∧ s ≤ r ⇒ FiniteRing s

subring_homo_homo

⊢ ∀r s r_ f. subring s r ∧ RingHomo f r r_ ⇒ RingHomo f s r_

subring_ids

⊢ ∀r s. s ≤ r ⇒ s.sum.id = #0 ∧ s.prod.id = #1

subring_mult

⊢ ∀r s. s ≤ r ⇒ ∀x y. x ∈ B ∧ y ∈ B ⇒ s.prod.op x y = x * y

subring_neg

⊢ ∀r s. s ≤ r ⇒ ∀x. x ∈ B ⇒ s.sum.inv x = -x

subring_num

⊢ ∀r s. s ≤ r ⇒ ∀n. s.sum.exp s.prod.id n = ##n

subring_one

⊢ ∀r s. s ≤ r ⇒ s.prod.id = #1

subring_prod_submonoid

⊢ ∀r s. subring s r ⇒ submonoid s.prod r.prod

subring_property

⊢ ∀r s.
    Ring s ∧ subring s r ⇒
    ∀x y. x ∈ B ∧ y ∈ B ⇒ s.sum.op x y = x + y ∧ s.prod.op x y = x * y

subring_refl

⊢ ∀r. subring r r

subring_ring_iso_compose

⊢ ∀r s r_ f. subring s r ∧ RingIso f r r_ ⇒ RingHomo f s r_

subring_ring_iso_ring_homo_subring

⊢ ∀r s r_ f. s ≤ r ∧ (r =r= r_) f ⇒ ring_homo_image f s r_ ≤ r_

subring_sub

⊢ ∀r s. s ≤ r ⇒ ∀x y. x ∈ B ∧ y ∈ B ⇒ ring_sub s x y = x − y

subring_sum_subgroup

⊢ ∀r s. subring s r ⇒ subgroup s.sum r.sum

subring_trans

⊢ ∀r s t. subring r s ∧ subring s t ⇒ subring r t

subring_unit

⊢ ∀r s. s ≤ r ⇒ ∀x. Unit s x ⇒ unit x

subring_unit_inv

⊢ ∀r s. s ≤ r ⇒ ∀x. Unit s x ⇒ Inv s x = |/ x

subring_unit_inv_element

⊢ ∀r s. s ≤ r ⇒ ∀x. Unit s x ⇒ Inv s x ∈ B

subring_unit_inv_nonzero

⊢ ∀r s. s ≤ r ∧ #1 ≠ #0 ⇒ ∀x. Unit s x ⇒ Inv s x ≠ #0

subring_unit_nonzero

⊢ ∀r s. s ≤ r ∧ #1 ≠ #0 ⇒ ∀x. Unit s x ⇒ x ≠ #0

subring_zero

⊢ ∀r s. s ≤ r ⇒ s.sum.id = #0

symdiff_eval

⊢ symdiff_set.carrier = 𝕌(:α -> bool) ∧
  (∀x y. symdiff_set.op x y = x ∪ y DIFF x ∩ y) ∧ symdiff_set.id = ∅

symdiff_set_inter_char

⊢ char symdiff_set_inter = 2

symdiff_set_inter_ring

⊢ Ring symdiff_set_inter

symdiff_univ_univ_eq_empty

⊢ symdiff 𝕌(:α) 𝕌(:α) = ∅

trivial_char

⊢ ∀z. char (trivial_ring z) = 1

trivial_integral_domain

⊢ ∀e0 e1. e0 ≠ e1 ⇒ FiniteIntegralDomain (trivial_integal_domain e0 e1)

trivial_ring

⊢ ∀z. FiniteRing (trivial_ring z)

trivial_ring_thm

⊢ ∀z. Ring (trivial_ring z)

unit_eq_refl

⊢ ∀r. Ring r ⇒ ∀x. x ∈ R ⇒ x =~ x

unit_eq_sym

⊢ ∀r. Ring r ⇒ ∀x y. x ∈ R ∧ y ∈ R ∧ x =~ y ⇒ y =~ x

unit_eq_trans

⊢ ∀r. Ring r ⇒ ∀x y z. x ∈ R ∧ y ∈ R ∧ z ∈ R ∧ x =~ y ∧ y =~ z ⇒ x =~ z

zero_ideal_ideal

⊢ ∀r. Ring r ⇒ <#0> << r

zero_ideal_sing

⊢ ∀r. Ring r ⇒ <#0>.carrier = {#0}

Theory ring

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems