Structures · Algebra
SMulCommClass
A typeclass mixin saying that two multiplicative actions on the same space commute.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Shape
- 3 explicit arguments · adds smul_comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Concrete types that are instances39
- Int
- Nat
- Real
- Rat
- NNReal
- ContinuousLinearMap
- BoundedContinuousFunction
- NNRat
- Matrix
- DomMulAct
- Units
- MonoidAlgebra
- AddMonoidAlgebra
- DirectLimit
- Matrix.SpecialLinearGroup
- Module.End
- AlgEquiv
- RingCon.Quotient
- CentroidHom
- LinearEquiv
- Circle
- ConjAct
- Complex.UnitClosedDisc
- Complex.UnitDisc
- SpecialLinearGroup
- RootPairing.Aut
- Subtype
- OrderDual
- Set.Elem
- MulOpposite
- PUnit
- Lex
- HasQuotient.Quotient
- ContinuousMap
- Multiplicative
- Submodule
- Set
- Finset
- Filter
How is a type an instance?
Loading the hierarchy index…
Assumed by2,671
- LinearMap.flip
- cfcₙ
- SMulCommClass.smul_comm
- Submodule.pointwiseDistribMulAction
- CFC.sqrt
- Algebra.TensorProduct.includeLeft
- SMulCommClass.symm
- mul_smul_comm
- cfcₙHom
- ContinuousLinearMap.mul
- LinearMap.mul
- DistribSMul.toLinearMap
- DoubleCentralizer.toProd
- LinearMap.mul'
- LinearMap.compr₂
- NonUnitalStarAlgebra.adjoin
- CFC.abs
- Finsupp.lsum
- LinearMap.compl₁₂
- LinearMap.compl₂
- Module.Basis.constr
- LinearMap.mulLeft
- KaehlerDifferential.map
- TensorProduct.tmul_smul
- QuadraticForm.tmul
- NonUnitalAlgebra.adjoin
- TensorProduct.AlgebraTensorModule.cancelBaseChange
- cfcₙ_apply
- Matrix.toLinearMap₂'
- cfcₙ_apply_of_not_predicate
- Unitary.conjStarAlgAut
- cfcₙ_congr
- LinearMap.mul_apply_apply
- LinearMap.toMatrix₂'
- QuadraticMap.sq
- TensorProduct.smul_tmul'
- Algebra.lsmul
- MeasureTheory.integral_smul
- DFinsupp.lsum
- cfcₙ_id
- NonUnitalStarAlgebra.elemental
- QuadraticMap.weightedSumSquares
- FixedPoints.intermediateField
- DistribSMul.toLinearMap_apply
- Module.Basis.constr_basis
- Rep.ofDistribMulAction
- TrivSqZeroExt.inlAlgHom
- LinearMap.ext₂
- SchwartzMap.seminorm
- LinearMap.lcomp
Ancestors0
No ancestors.