card_classGroup_eq_one_iff
theorem card_classGroup_eq_one_iff :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDedekindDomain R]
[inst_3 : Fintype (ClassGroup R)], Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R
The theorem `card_classGroup_eq_one_iff` asserts that for any commutative ring `R` which is a domain and a Dedekind domain, if the class group of `R` is finite (i.e., it has a finite number of elements), then the number of elements in the class group of `R` is `1` if and only if `R` is a principal ideal ring. In other words, the class number (which is the cardinality of the class group) of a ring of integers being `1` is equivalent to the ring of integers being a principal ideal domain.
More concisely: For a commutative domain and Dedekind domain R, the class group of R has order 1 if and only if R is a principal ideal ring.
|
ClassGroup.mk_eq_one_iff
theorem ClassGroup.mk_eq_one_iff :
∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ},
ClassGroup.mk I = 1 ↔ (↑↑I).IsPrincipal
The theorem `ClassGroup.mk_eq_one_iff` states that for any commutative ring `R`, field `K`, and a non-zero fractional ideal `I` of `R` in `K`, the class of `I` in the class group is one if and only if `I` is a principal ideal. Here, `R` is assumed to be an integral domain and `K` is the field of fractions of `R`. In mathematical terms, this theorem indicates that the isomorphism class of a non-zero fractional ideal under the operation of ideal multiplication is trivial in the class group precisely when the ideal itself is principal.
More concisely: A non-zero fractional ideal in the field of fractions of a commutative domain is in the trivial class of the class group if and only if it is principal.
|
card_classGroup_eq_one
theorem card_classGroup_eq_one :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R],
Fintype.card (ClassGroup R) = 1
This theorem states that the class number of a principal ideal domain is `1`. In other words, for any type `R` that is a commutative ring, a domain, and a principal ideal ring, the cardinality (or number of elements) of the class group of `R` is `1`. A class group is defined here as the group of invertible fractional ideals modulo the principal ideals. The theorem implies that in a principal ideal domain, all invertible fractional ideals are essentially the same, up to principal ideals.
More concisely: In a principal ideal domain, the class group, which is the group of invertible fractional ideals modulo principal ideals, has order 1.
|
ClassGroup.induction
theorem ClassGroup.induction :
∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] {P : ClassGroup R → Prop},
(∀ (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ), P (ClassGroup.mk I)) → ∀ (x : ClassGroup R), P x
The theorem `ClassGroup.induction` represents an induction principle for the class group. Specifically, it states that in order to prove that a property `P` holds for all elements `x` of the class group `ClassGroup R` of a commutative ring `R`, it suffices to select a fraction field `K` and demonstrate that the property `P` holds true for the equivalence class of each non-zero fractional ideal `I` in `FractionalIdeal R⁰ K`. This induction principle allows us to reduce a problem about a class group to a simpler problem about fractional ideals.
More concisely: The theorem `ClassGroup.induction` in Lean 4 states that to prove a property holds for all elements in the class group of a commutative ring, it's sufficient to show it holds for the equivalence classes of non-zero fractional ideals in the ring's fraction field.
|