Theorems · Inductive type · group theory
MulZeroClass
Type u → Type u
Typeclass for expressing that a type M₀ with multiplication and a zero satisfies
0 * a = 0 and a * 0 = 0 for all a : M₀.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 232 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 by255
Results whose statement or proof uses this declaration.
- MulZeroClass.mul_zerostatement and proof · cited by 2,091
- MulZeroClass.zero_mulstatement and proof · cited by 1,625
- mul_nonnegstatement · cited by 397
- mul_posstatement · cited by 374
- mul_eq_zerostatement and proof · cited by 94
- mul_ne_zero_iffstatement and proof · cited by 39
- right_ne_zero_of_mulstatement and proof · cited by 38
- left_ne_zero_of_mulstatement and proof · cited by 27
- mul_nonpos_of_nonpos_of_nonnegstatement and proof · cited by 24
- mul_nonpos_of_nonneg_of_nonposstatement and proof · cited by 21
- mul_eq_zero_of_rightstatement and proof · cited by 16
- IsRegular.of_ne_zerostatement and proof · cited by 15
Showing the 200 most cited of 255.