Theorems · Inductive type · group theory
GroupWithZero
Type u → Type u
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
- Cited by
- 691 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by750
Results whose statement or proof uses this declaration.
- div_posstatement and proof · cited by 337
- inv_mul_cancel₀statement and proof · cited by 267
- div_zerostatement and proof · cited by 251
- div_selfstatement and proof · cited by 237
- zero_divstatement and proof · cited by 222
- mul_inv_cancel₀statement and proof · cited by 210
- inv_zerostatement and proof · cited by 184
- Units.mk0statement and proof · cited by 181
- inv_posstatement and proof · cited by 124
- inv_pos_of_posstatement and proof · cited by 123
- div_mul_cancel₀statement and proof · cited by 122
- map_inv₀statement and proof · cited by 106
Showing the 200 most cited of 750.