associated_coe — Mathlib

English

For elements a,b of M₀⁰, being associated after coercion to M₀ is equivalent to being associated in M₀ itself: Associated (a : M0) b ↔ Associated a b.

Русский

Для элементов a,b ∈ M0⁰ равенство связанные по переносу в M0 эквивалентно тому, что a и b ассоциированы в M0.

LaTeX

$$associated_coe : Associated (a : M0) b ↔ Associated a b$$

Lean4

@[simp, norm_cast]
theorem associated_coe : Associated (a : M₀) b ↔ Associated a b :=
  unitsNonZeroDivisorsEquiv.symm.exists_congr_left.trans <| by simp [Associated]; norm_cast

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