not_separatingLeft_zero — Mathlib

English

If B.SeparatingLeft holds, then B ≠ 0 for a nontrivial module; equivalently, a separating left form cannot be the zero form.

Русский

Если B разделяет слева, то B не равно нулю; эквивалентно тому, что нулевая форма не может быть разделяющей слева.

LaTeX

$$B.SeparatingLeft → B ≠ 0$$

Lean4

/-- In a non-trivial module, zero is not non-degenerate. -/
theorem not_separatingLeft_zero [Nontrivial M₁] : ¬(0 : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M).SeparatingLeft :=
  let ⟨m, hm⟩ := exists_ne (0 : M₁)
  fun h ↦ hm (h m fun _n ↦ rfl)

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