ne_zero_of_ortho — Mathlib

English

Under the same orthogonality-type condition, x ≠ 0.

Русский

При условии, аналогичном ортогональности, x ≠ 0.

LaTeX

$$$\\forall x,N,\\, ( \\forall c \\in R, \\forall y \\in N, c x + y = 0 \\Rightarrow c = 0 ) \\Rightarrow x \\neq 0$$$

Lean4

theorem ne_zero_of_ortho {x : M} {N : Submodule R M} (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = (0 : M) → c = 0) :
    x ≠ 0 :=
  mt (fun h => show x ∈ N from h.symm ▸ N.zero_mem) (notMem_of_ortho ortho)

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