unitsEquivNeZero — Mathlib

English

In a GroupWithZero, the unit group G₀ˣ is canonically equivalent to the set of nonzero elements {a ∈ G₀ | a ≠ 0}.

Русский

В группе с нулём единицы G₀ˣ эквивалентны множеству ненулевых элементов {a ∈ G₀ | a ≠ 0}.

LaTeX

$$$G_0^{\\times} \\simeq \\{ a \\in G_0 \\mid a \\neq 0 \\}$$$

Lean4

/-- In a `GroupWithZero` `G₀`, the unit group `G₀ˣ` is equivalent to the subtype of nonzero
elements. -/
@[simps]
def _root_.unitsEquivNeZero : G₀ˣ ≃ { a : G₀ // a ≠ 0 }
    where
  toFun a := ⟨a, a.ne_zero⟩
  invFun a := Units.mk0 _ a.prop

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