canonicalEquiv_mk0 — Mathlib

English

Canonical equivalence is compatible with mk0 across different fraction fields.

Русский

Каноническое эквивалентство совместимо с mk0 для разных полей дробей.

LaTeX

$$$\mathrm{canonicalEquiv}_{R^{0},K,K'} \circ \mathrm{mk0}_{K} = \mathrm{mk0}_{K'}. $$$

Lean4

theorem canonicalEquiv_mk0 [IsDedekindDomain R] (K' : Type*) [Field K'] [Algebra R K'] [IsFractionRing R K']
    (I : (Ideal R)⁰) : FractionalIdeal.canonicalEquiv R⁰ K K' (FractionalIdeal.mk0 K I) = FractionalIdeal.mk0 K' I := by
  simp only [FractionalIdeal.coe_mk0, FractionalIdeal.canonicalEquiv_coeIdeal]

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