exists_iff_ne_zero — Mathlib

English

The statement exists_iff_ne_zero: there exists a unit with property p is equivalent to there exists a nonzero element x with p(x).

Русский

Существование единицы с свойством p эквивалентно существованию ненулевого элемента x с свойством p.

LaTeX

$$$(\exists u:G_0^\times, p(u)) \iff (\exists x \neq 0, p(x))$$$

Lean4

@[simp]
theorem exists_iff_ne_zero {p : G₀ → Prop} : (∃ u : G₀ˣ, p u) ↔ ∃ x ≠ 0, p x := by simp [exists0]

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