algebraMap_mk_of_liesOver — Mathlib

English

The canonical algebra map on quotients satisfies the compatibility: algebraMap_{A/p,B/P}(mk p x) = mk_P(algebraMap_{A,B} x).

Русский

Каноническое отображение алгебры на частоте совместимо: algebraMap_{A/p,B/P}(mk p x) = mk_P(algebraMap_{A,B} x).

LaTeX

$$$ algebraMap (A \\,/\\ p) (B \\,/\\ P) (Ideal.Quotient.mk p x) = Ideal.Quotient.mk P (algebraMap A B x). $$$

Lean4

@[simp]
theorem algebraMap_mk_of_liesOver (x : A) :
    algebraMap (A ⧸ p) (B ⧸ P) (Ideal.Quotient.mk p x) = Ideal.Quotient.mk P (algebraMap _ _ x) :=
  rfl

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