Mathlib Map

Theorems · Definition · group theory

Monoid.toOne

{M : Type u} → [self : Monoid M] → One M
Defined in
Mathlib.Algebra.Group.Defs
Cited by
34 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Monoid.ext · cited by 7Monoid.extRing.ext · cited by 5Ring.extSemiring.ext · cited by 5Semiring.extRCLike.I_mul_I_ax · cited by 3RCLike.I_mul_I_axDivisionMonoid.inv_eq_of_mul · cited by 2DivisionMonoid.inv_eq_of_…Group.casesOn · cited by 2Group.casesOnMonoid.npow_zero · cited by 1Monoid.npow_zeroGroup.inv_mul_cancel · cited by 1Group.inv_mul_cancelCommGroupWithZero.mul_inv_cancel · cited by 1CommGroupWithZero.mul_inv…ESeminormedMonoid.enorm_zero · cited by 1ESeminormedMonoid.enorm_z…Semiring.casesOn · cited by 1Semiring.casesOnDivisionRing.mul_inv_cancel · cited by 1DivisionRing.mul_inv_canc…GroupWithZero.mul_inv_cancel · cited by 1GroupWithZero.mul_inv_can…DivInvMonoid.casesOn · cited by 1DivInvMonoid.casesOnDivInvMonoid.zpow_zero' · cited by 1DivInvMonoid.zpow_zero'Monoid · cited by 3887MonoidMonoid.toOneCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Monoidstatement and proof · cited by 3,887

Cited by85

Results whose statement or proof uses this declaration.