injective_stableUnderComposition — Mathlib

English

The property of being injective is stable under composition of ring homomorphisms.

Русский

Свойство инъективности устойчиво к композиции кольцевых гомоморфизмов.

LaTeX

$$$\\text{StableUnderComposition}\\; (\\lambda f. \\text{Injective}(f))$$$

Lean4

theorem _root_.RingHom.injective_stableUnderComposition :
    RingHom.StableUnderComposition (fun f ↦ Function.Injective f) :=
  by
  intro R S T _ _ _ f g hf hg
  simp only [RingHom.coe_comp]
  exact Function.Injective.comp hg hf

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