Structures · Algebra
Monoid
A Monoid is a Semigroup with an element 1 such that 1 * a = a * 1 = a.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds one_mul, mul_one, npow_zero, npow_succ
Extends3
Extended by8
Forgetful instances
Concrete types that are instances90
- Int
- Nat
- Real
- Rat
- SeparationQuotient
- Filter.Germ
- BoundedContinuousFunction
- Unitization
- WithConv
- LocallyConstant
- DomMulAct
- Units
- MeasureTheory.SimpleFunc
- RestrictedProduct
- TrivSqZeroExt
- DirectLimit
- UniformFun
- Zsqrtd
- UniformOnFun
- ContMDiffMap
- LocalizedModule
- OreLocalization
- CategoryTheory.Limits.Cone.pt
- LucasLehmer.X
- CategoryTheory.End
- Tropical
- Ordinal
- ArithmeticFunction
- Matrix.SpecialLinearGroup
- Module.End
- MeasureTheory.AEEqFun
- Representation.IntertwiningMap
- RingCon.Quotient
- MulActionHom
- AddMonoid.End
- GradedTensorProduct
- OneHom
- CategoryTheory.Skeleton
- ProbabilityTheory.Kernel
- AlgHom
- MonCat.carrier
- GradedAlgHom
- BialgHom
- AffineMap
- SubMulAction
- NonUnitalStarAlgHom
- CoalgHom
- GroupLike
- Con.Quotient
- RelEmbedding
- OrderType
- Monoid.CoprodI
- RootPairing.Equiv
- Monoid.PushoutI
- Monoid.Coprod
- StarAlgHom
- ContinuousAlgHom
- RelHom
- CircleDeg1Lift
- NonUnitalStarRingHom
- GradedRingHom
- AddConstMap
- LinearIsometry
- StarMonoidHom
- GradedMonoid
- Monoid.End
- Dilation
- AffineIsometry
- PreQuasiregular
- Function.End
- RootPairing.Hom
- MonCat.Colimits.ColimitType
- CategoryTheory.Conv
- MonCat.FilteredColimits.M
- PresentedMonoid
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Shrink
- Colex
- Multiplicative
- OrderHom
- RingHom
- WithOne
How is a type an instance?
Loading the hierarchy index…
Assumed by5,398
- Units.val
- IsUnit
- one_smul
- pow_zero
- pow_one
- Rep.V
- one_pow
- map_pow
- Submonoid.powers
- Representation
- pow_succ
- smul_smul
- Rep.ρ
- orderOf
- pow_add
- Associated
- sq
- IsUnit.unit
- pow_succ'
- Rep.res
- pow_mul
- Associates
- unitary
- Representation.IntertwiningMap.toLinearMap
- Rep.Hom.hom
- Action.V
- emultiplicity
- pow_two
- IsRelPrime
- Monoid.exponent
- multiplicity
- Units.isUnit
- IsOfFinOrder
- Squarefree
- Submodule.pointwiseDistribMulAction
- IsUnit.map
- Representation.tprod
- Even.neg_pow
- dvd_refl
- Units.map
- Set.mulActionSet
- OreLocalization
- Associated.symm
- Action.Hom.hom
- dvd_rfl
- NonUnitalAlgHomClass
- IsStrictlyPositive
- FiniteMultiplicity
- OreLocalization.oreDiv
- Units.mul_inv