notMem_of_ortho — Mathlib

English

If for a fixed x ∈ M and a submodule N, the only scalar c ∈ R that can satisfy c x + y = 0 for some y ∈ N is c = 0, then x ∉ N.

Русский

Пусть x ∈ M и N — подпомодуль. Если для данного x и N для всех c ∈ R и y ∈ N равенство c x + y = 0 может выполняться только тогда, когда c = 0, то x ∉ N.

LaTeX

$$$\\forall c \\in R, \\forall y \\in N, c \\cdot x + y = 0 \\Rightarrow c = 0 \\;\;\\Rightarrow\\; x \\notin N$$$

Lean4

theorem notMem_of_ortho {x : M} {N : Submodule R M} (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = (0 : M) → c = 0) : x ∉ N :=
  by
  intro hx
  simpa using ortho (-1) x hx

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