equiv_mk0 — Mathlib

English

Every class in the class group is represented by some nonzero ideal via mk0.

Русский

Каждый класс в группе классов имеет представление как mk0 от ненулевого идеала.

LaTeX

$$$\text{Surjective}~(\mathrm{ClassGroup.mk0})$$$

Lean4

@[simp]
theorem equiv_mk0 [IsDedekindDomain R] (I : (Ideal R)⁰) :
    ClassGroup.equiv K (ClassGroup.mk0 I) = QuotientGroup.mk' (toPrincipalIdeal R K).range (FractionalIdeal.mk0 K I) :=
  by
  rw [ClassGroup.mk0, MonoidHom.comp_apply, ClassGroup.equiv_mk]
  congr 1
  simp [← Units.val_inj]

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