Theorems · Definition · group theory

WithZero.withZeroUnitsEquiv

{G : Type u_4} → [inst : GroupWithZero G] → [DecidablePred fun a => a = 0] → WithZero Gˣ ≃* G

Any group with zero is isomorphic to adjoining 0 to the units of itself.

Defined in

Mathlib.Algebra.GroupWithZero.WithZero

Cited by

9 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupWithZeroDecidablePred