quotient_map_C_eq_zero — Mathlib

English

If I is an ideal of R, and a ∈ I, then the composite map (Quotient.mk I) ∘ C sends a to 0 in R[X]/I.

Русский

Если I — идеал R и a ∈ I, то композиция (Quotient.mk I) ∘ C отправляет a в 0 в R[X]/I.

LaTeX

$$$\\forall a ∈ I:\\, ((\\Quotient.mk I).comp C) a = 0$$$

Lean4

theorem quotient_map_C_eq_zero {I : Ideal R} :
    ∀ a ∈ I, ((Quotient.mk (map (C : R →+* R[X]) I : Ideal R[X])).comp C) a = 0 :=
  by
  intro a ha
  rw [RingHom.comp_apply, Quotient.eq_zero_iff_mem]
  exact mem_map_of_mem _ ha

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