mk_mk0 — Mathlib

English

The class of a fractional ideal under mk0 agrees with the class obtained by applying mk0 after representing the ideal by mk0.

Русский

Класс дробного идеала под mk0 согласуется с классом, полученным после применения mk0 после представления идеала через mk0.

LaTeX

$$$\mathrm{ClassGroup.mk}(\mathrm{FractionalIdeal.mk0}(K,I)) = \mathrm{ClassGroup.mk0}(I).$$$

Lean4

@[simp]
theorem mk_mk0 [IsDedekindDomain R] (I : (Ideal R)⁰) : ClassGroup.mk (FractionalIdeal.mk0 K I) = ClassGroup.mk0 I := by
  rw [ClassGroup.mk0, MonoidHom.comp_apply, ← ClassGroup.mk_canonicalEquiv K (FractionRing R),
    FractionalIdeal.map_canonicalEquiv_mk0]

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