ne_zero_of_injective — Mathlib

English

Let M be a nontrivial module. If f: M →ₛₗ[σ₁₂] M₂ is injective, then f ≠ 0.

Русский

Пусть M ненулевой модуль. Тогда для любого f: M →ₛₗ[σ₁₂] M₂ инъективного типа следует, что f ≠ 0.

LaTeX

$$$[Nontrivial M] \Rightarrow (\text{Injective } f) \Rightarrow f \neq 0$$$

Lean4

theorem ne_zero_of_injective [Nontrivial M] {f : M →ₛₗ[σ₁₂] M₂} (hf : Injective f) : f ≠ 0 :=
  have ⟨x, ne⟩ := exists_ne (0 : M)
  fun h ↦ hf.ne ne <| by simp [h]

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