exists0' — Mathlib

English

An alternative version of exists0: (∃ g: G₀, g ≠ 0, p g g.ne_zero) ↔ ∃ u: G₀ˣ, p u u.ne_zero.

Русский

Альтернативная версия exists0: (существует g ≠ 0 с p(g,g.ne_zero)) эквивалентно существованию единицы u с p(u) и u.ne_zero.

LaTeX

$$$\Bigl(\exists g:G_0,\ g\neq 0,\ p\ g\ g.\text{ne\_zero}}\Bigr) \iff (\exists u:G_0^\times,\ p(u)\ u.ne\_zero)$$$

Lean4

/-- An alternative version of `Units.exists0`. This one is useful if Lean cannot
figure out `p` when using `Units.exists0` from right to left. -/
theorem exists0' {p : ∀ g : G₀, g ≠ 0 → Prop} : (∃ (g : G₀) (hg : g ≠ 0), p g hg) ↔ ∃ g : G₀ˣ, p g g.ne_zero :=
  Iff.trans (by simp_rw [val_mk0]) exists0.symm

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