Quot_mk_eq_mk — Mathlib

English

The quotient representative of I equals mk I in the class group; i.e., the natural quotient map sends I to the same class as mk I.

Русский

Представитель в фактор-группе I совпадает по классу с mk I; естественный переход в факторгруппу отправляет I в тот же класс, что и mk I.

LaTeX

$$$\operatorname{Quot.mk}_{\mathsf{leftRel}}(\mathrm{toPrincipalIdeal}(R,\mathrm{FractionRing}(R)).range).r(I) = \mathrm{ClassGroup.mk}(I).$$$

Lean4

theorem Quot_mk_eq_mk (I : (FractionalIdeal R⁰ (FractionRing R))ˣ) : Quot.mk _ I = ClassGroup.mk I :=
  by
  rw [ClassGroup.mk_def, canonicalEquiv_self, RingEquiv.coe_monoidHom_refl, Units.map_id, MonoidHom.id_apply,
    QuotientGroup.mk'_apply]
  rfl

Похожие утверждения