Theorems · Theorem · commutative algebra

ClassGroup.mk_eq_mk_of_coe_ideal

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R]
  {I J : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {I' J' : Ideal R},
  ↑I = ↑I' →
    ↑J = ↑J' →
      ((ClassGroup.mk (FractionRing R)) I = (ClassGroup.mk (FractionRing R)) J ↔
        ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J')

Defined in: Mathlib.RingTheory.ClassGroup.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsDomain

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites36

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
CommRingstatement and proof · cited by 17,173
Algebraproof · cited by 11,388
Idealstatement and proof · cited by 4,748
MonoidHomstatement · cited by 3,629
Submonoidproof · cited by 3,086
Unitsstatement and proof · cited by 2,804
mul_commproof · cited by 2,262
IsDomainstatement and proof · cited by 2,196
Units.valstatement and proof · cited by 1,966
IsUnitproof · cited by 1,602

Cited by2

Results whose statement or proof uses this declaration.

ClassGroup.mk_eq_one_of_coe_idealproof · cited by 2
WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'proof · cited by 0