Theorems · Definition · commutative algebra
ClassGroup.mulEquivUnitsSubmoduleQuotRange
(R : Type u_1) →
[inst : CommRing R] →
[inst_1 : IsDomain R] →
ClassGroup R ≃* (Submodule R (FractionRing R))ˣ ⧸ (Units.map ↑(Submodule.spanSingleton R)).rangeThe class group of R is isomorphic to the group of invertible R-submodules in Frac(R)
modulo the principal submodules (invertible submodules are automatically fractional ideals).
- Defined in
- Mathlib.RingTheory.ClassGroup.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
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
- Submodulestatement · cited by 7,192
- Subgroupstatement · cited by 3,593
- Unitsstatement · cited by 2,804
- HasQuotient.Quotientstatement · cited by 2,301
- IsDomainstatement and proof · cited by 2,196
- MulEquivstatement · cited by 1,142
- nonZeroDivisorsstatement · cited by 895
- MonoidHom.rangestatement and proof · cited by 314
- FractionRingstatement and proof · cited by 200
- Units.mapstatement and proof · cited by 95
- ClassGroupstatement · cited by 50
Cited by3
Results whose statement or proof uses this declaration.
- ClassGroup.equivPicproof · cited by 2
- ClassGroup.equivPic_applystatement · cited by 0
- ClassGroup.equivPic_symm_applystatement · cited by 0