Theorems · Definition · commutative algebra
ClassGroup
(R : Type u_1) → [inst : CommRing R] → [IsDomain R] → Type u_1
The ideal class group of R is the group of invertible fractional ideals
modulo the principal ideals.
- Defined in
- Mathlib.RingTheory.ClassGroup.Basic
- Cited by
- 50 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Unitsproof · cited by 2,804
- HasQuotient.Quotientproof · cited by 2,301
- IsDomainstatement and proof · cited by 2,196
- nonZeroDivisorsproof · cited by 895
- FractionalIdealproof · cited by 423
- MonoidHom.rangeproof · cited by 314
- FractionRingproof · cited by 200
- toPrincipalIdealproof · cited by 23
Cited by63
Results whose statement or proof uses this declaration.
- ClassGroup.mkstatement · cited by 22
- ClassGroup.mk0statement · cited by 22
- NumberField.classNumberproof · cited by 7
- ClassGroup.extendedHomstatement · cited by 7
- ClassGroup.equivstatement · cited by 6
- WeierstrassCurve.Affine.Point.toClassstatement and proof · cited by 5
- ClassGroup.mk0_surjectivestatement and proof · cited by 5
- ClassGroup.mk0_eq_one_iffstatement · cited by 4
- ClassGroup.mk_defstatement · cited by 4
- ClassGroup.mk_eq_one_iffstatement · cited by 4
- ClassGroup.Quot_mk_eq_mkstatement and proof · cited by 3
- ClassGroup.mk_mk0statement and proof · cited by 3