Structures · Algebra

CommGroupWithZero

A type G₀ is a commutative “group with zero” if it is a commutative monoid with zero element (distinct from 1) such that every nonzero element is invertible. The type is required to come with an “inverse” function, and the inverse of 0 must be 0.

Defined in

Mathlib.Algebra.GroupWithZero.Defs

Shape

One type argument · adds div_eq_mul_inv, zpow_zero', zpow_succ', zpow_neg', inv_zero, mul_inv_cancel