Theorems · Inductive type · group theory
SMulCommClass
(M : Type u_9) → (N : Type u_10) → (α : Type u_11) → [SMul M α] → [SMul N α] → Prop
A typeclass mixin saying that two multiplicative actions on the same space commute.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 1,927 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 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 by2,281
Results whose statement or proof uses this declaration.
- NonUnitalContinuousFunctionalCalculusstatement · cited by 275
- LinearMap.flipstatement and proof · cited by 193
- cfcₙstatement · cited by 187
- SMulCommClass.smul_commstatement and proof · cited by 143
- Submodule.pointwiseDistribMulActionstatement and proof · cited by 105
- CFC.sqrtstatement and proof · cited by 82
- Algebra.TensorProduct.includeLeftstatement and proof · cited by 72
- NonUnitalIsometricContinuousFunctionalCalculusstatement · cited by 68
- SMulCommClass.symmstatement and proof · cited by 67
- cfcₙHomstatement and proof · cited by 65
- mul_smul_commstatement and proof · cited by 65
- ContinuousLinearMap.mulstatement and proof · cited by 63
Showing the 200 most cited of 2,281.