Theorems · Theorem · group theory

WithZero.withZeroUnitsEquiv_symm_apply

∀ {G : Type u_4} [inst : GroupWithZero G] [inst_1 : DecidablePred fun a => a = 0] (a : G),
  WithZero.withZeroUnitsEquiv.symm a = if h : a = 0 then 0 else ↑(Units.mk0 a h)

Defined in

Mathlib.Algebra.GroupWithZero.WithZero

Cited by

3 results in Mathlib

Foundations

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

Assumes

GroupWithZeroDecidablePred