ne_zero_iff — Mathlib

English

Let p be a ring seminorm on a nonunital ring R. Then p is nonzero if and only if there exists x ∈ R such that p(x) ≠ 0.

Русский

Пусть p — кольцевой семинорм на кольце без единицы R. Тогда p ≠ 0 тогда же, когда существует элемент x ∈ R such that p(x) ≠ 0.

LaTeX

$$$ p \neq 0 \iff \exists x \in R: p(x) \neq 0 $$$

Lean4

theorem ne_zero_iff {p : RingSeminorm R} : p ≠ 0 ↔ ∃ x, p x ≠ 0 := by simp [eq_zero_iff]

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