withZeroUnitsEquiv

Mathlib.Algebra.GroupWithZero.WithZero

URI: https://scilib.ai/kg/mathlib#WithZero.withZeroUnitsEquiv

Lean4

/-- Any group with zero is isomorphic to adjoining `0` to the units of itself. -/
@[simps]
def withZeroUnitsEquiv {G : Type*} [GroupWithZero G] [DecidablePred (fun a : G ↦ a = 0)] : WithZero Gˣ ≃* G
    where
  toFun := WithZero.recZeroCoe 0 Units.val
  invFun a := if h : a = 0 then 0 else (Units.mk0 a h : Gˣ)
  left_inv := (by induction · <;> simp)
  right_inv _ := by simp only; split <;> simp_all
  map_mul' := (by induction · <;> induction · <;> simp [← WithZero.coe_mul])

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru