Structures · Algebra
GroupWithZero
A type G₀ is a “group with zero” if it is a 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.
Examples include division rings and the ordered monoids that are the
target of valuations in general valuation theory.
- 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
Extends3
Extended by2
Forgetful instances
Every GroupWithZero is also a
Concrete types that are instances16
- Filter.Germ
- Quaternion
- DirectLimit
- Polynomial.SplittingField
- AlgebraicClosure
- AdjoinRoot
- OreLocalization
- ConjAct
- GrpWithZero.carrier
- Subtype
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by761
- div_pos
- inv_mul_cancel₀
- div_zero
- div_self
- zero_div
- mul_inv_cancel₀
- inv_zero
- Units.mk0
- inv_pos
- inv_pos_of_pos
- div_mul_cancel₀
- map_inv₀
- div_nonneg
- inv_ne_zero
- Ne.isUnit
- map_div₀
- div_le_iff₀
- inv_smul_smul₀
- div_le_div_of_nonneg_right
- le_div_iff₀
- smul_inv_smul₀
- Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos
- inv_nonneg
- div_le_div₀
- MonoidWithZeroHom.ValueGroup₀.embedding
- inv_mul_cancel_left₀
- div_lt_iff₀
- lt_div_iff₀
- invOf_eq_inv
- mul_inv_cancel_left₀
- eq_div_iff
- div_eq_iff
- IsUnit.mk0
- MonoidWithZeroHom.ValueGroup₀.restrict₀
- div_le_one_of_le₀
- mul_inv_cancel_right₀
- isUnit_iff_ne_zero
- zpow_ne_zero
- zpow_add₀
- div_ne_zero
- Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg
- Set.mem_smul_set_iff_inv_smul_mem₀
- inv_anti₀
- one_div_pos
- inv_mul_cancel_right₀
- map_zpow₀
- OrderIso.mulLeft₀
- inv_nonneg_of_nonneg
- inv_le_inv₀
- Filter.Tendsto.div