ker_eq_bot_of_inverse — Mathlib

English

ker_eq_bot' is equivalent to: f is injective.

Русский

ker_eq_bot' эквивалентно: f инъективно.

LaTeX

$$ker f = ⊥' iff ∀ m, f m = 0 → m = 0$$

Lean4

theorem ker_eq_bot_of_inverse {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₁] M}
    (h : (g.comp f : M →ₗ[R] M) = id) : ker f = ⊥ :=
  ker_eq_bot'.2 fun m hm => by rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]

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