English
Taking I through canonicalEquiv and then mk yields the same class as mk I.
Русский
Промежуточное прохождение I через canonicalEquiv и затем через mk даёт тот же класс, что и mk I.
LaTeX
$$$\mathrm{ClassGroup.mk}(\mathrm{Units.map}(\uparrow(\mathrm{canonicalEquiv}(R^{0},K,K')))\,I) = \mathrm{ClassGroup.mk}(I).$$$
Lean4
@[simp]
theorem mk_canonicalEquiv (K' : Type*) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : (FractionalIdeal R⁰ K)ˣ) :
ClassGroup.mk (Units.map (↑(canonicalEquiv R⁰ K K')) I : (FractionalIdeal R⁰ K')ˣ) = ClassGroup.mk I := by
rw [ClassGroup.mk_def, ClassGroup.mk_def, ← MonoidHom.comp_apply (Units.map _), ← Units.map_comp, ←
RingEquiv.coe_monoidHom_trans, FractionalIdeal.canonicalEquiv_trans_canonicalEquiv]
