map_canonicalEquiv_mk0 — Mathlib

English

Applying Units.map to canonicalEquiv and then mk0 recovers mk0.

Русский

Применение Units.map к canonicalEquiv и затем mk0 восстанавливает mk0.

LaTeX

$$$\mathrm{Units.map}(\uparrow(\mathrm{canonicalEquiv}(R^{0},K,K')))\big(\mathrm{FractionalIdeal.mk0}(K,I)\big) = \mathrm{FractionalIdeal.mk0}(K',I).$$$

Lean4

@[simp]
theorem map_canonicalEquiv_mk0 [IsDedekindDomain R] (K' : Type*) [Field K'] [Algebra R K'] [IsFractionRing R K']
    (I : (Ideal R)⁰) :
    Units.map (↑(FractionalIdeal.canonicalEquiv R⁰ K K')) (FractionalIdeal.mk0 K I) = FractionalIdeal.mk0 K' I :=
  Units.ext (FractionalIdeal.canonicalEquiv_mk0 K K' I)

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