English
In a group with zero, an existential over a unit with property p is equivalent to the existence of a nonzero element g with p(Units.mk0 g hg).
Русский
В группе с нулём существование единицы с свойством p эквивалентно существованию ненулевого элемента g с p(Units.mk0 g hg).
LaTeX
$$$(\exists g:G_0^\times, p(g)) \iff (\exists g:G_0, g \neq 0, p(\text{Units.mk0 } g\, g.\text{ne\_zero}))$$$
Lean4
/-- In a group with zero, an existential over a unit can be rewritten in terms of `Units.mk0`. -/
theorem exists0 {p : G₀ˣ → Prop} : (∃ g : G₀ˣ, p g) ↔ ∃ (g : G₀) (hg : g ≠ 0), p (Units.mk0 g hg) :=
⟨fun ⟨g, pg⟩ => ⟨g, g.ne_zero, (g.mk0_val g.ne_zero).symm ▸ pg⟩, fun ⟨g, hg, pg⟩ => ⟨Units.mk0 g hg, pg⟩⟩
