piQuotientEquiv_map — Mathlib

English

The action of piQuotientEquiv on the image of x ∈ S under the quotient corresponds to the image under the corresponding quotient map on each component.

Русский

Действие piQuotientEquiv на образ x через факторизацию сопоставляет образ через соответствующий фактор в каждой компоненте.

LaTeX

$$$\\\\text{piQuotientEquiv} p hp (Ideal.Quotient.mk _ x) = fun _ => Ideal.Quotient.mk _ x$$$

Lean4

@[simp]
theorem piQuotientEquiv_map (p : Ideal R) (hp : map (algebraMap R S) p ≠ ⊥) (x : R) :
    Factors.piQuotientEquiv p hp (algebraMap _ _ x) = fun _ => Ideal.Quotient.mk _ (algebraMap _ _ x) :=
  rfl

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