injective_respectsIso — Mathlib

English

Injectivity respects isomorphisms: if f is injective, then under isomorphisms it remains injective.

Русский

Инъективность сохраняется при изоморфизмах: если f инъективен, то под изоморфизмами он останется инъективным.

LaTeX

$$$\\text{RespectsIso}(\\text{Injective})$$$

Lean4

theorem _root_.RingHom.injective_respectsIso : RingHom.RespectsIso (fun f ↦ Function.Injective f) :=
  by
  apply RingHom.injective_stableUnderComposition.respectsIso
  intro R S _ _ e
  exact e.bijective.injective

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