map_ne_zero_iff — Mathlib

English

Let e be a semilinear equivalence between modules M and M₂. Then e preserves nonzeroness: for every x in M, x ≠ 0 if and only if e(x) ≠ 0.

Русский

Пусть e — полупрямой линейный эквивалент между модулями M и M₂. Тогда он сохраняет ненулевой вектор: для каждого x ∈ M верно, что x ≠ 0 тогда и только тогда, когда e(x) ≠ 0.

LaTeX

$$$\\forall x\\; (e\,x \\neq 0) \\iff x \\neq 0$$$

Lean4

theorem map_ne_zero_iff {x : M} : e x ≠ 0 ↔ x ≠ 0 :=
  e.toAddEquiv.map_ne_zero_iff

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