Theorems · Theorem · group theory
SMulCommClass.of_commMonoid
∀ (A : Type u_9) (B : Type u_10) (G : Type u_11) [inst : CommMonoid G] [inst_1 : SMul A G] [inst_2 : SMul B G] [IsScalarTower A G G] [IsScalarTower B G G], SMulCommClass A B G
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsScalarTowerstatement and proof · cited by 3,896
- CommMonoidstatement and proof · cited by 2,264
- SMulCommClassstatement · cited by 1,927
- one_smulproof · cited by 1,374
- smul_assocproof · cited by 150
- SMulCommClass.smul_commproof · cited by 143
Cited by49
Results whose statement or proof uses this declaration.
- Algebra.Extension.CotangentSpace.mapstatement · cited by 25
- Algebra.Generators.H1Cotangent.δAuxstatement · cited by 10
- Algebra.Extension.CotangentSpace.map_tmulstatement · cited by 7
- KaehlerDifferential.tensorKaehlerEquivBasestatement · cited by 7
- Algebra.Extension.CotangentSpace.map_cotangentComplexstatement · cited by 4
- Algebra.Generators.CotangentSpace.compEquiv_symm_inrstatement · cited by 4
- Algebra.Generators.CotangentSpace.map_toComp_injectivestatement · cited by 4
- Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChangestatement · cited by 4
- KaehlerDifferential.moduleBaseChange'statement · cited by 4
- KaehlerDifferential.derivationTensorProductstatement · cited by 3
- Algebra.Generators.CotangentSpace.exactstatement · cited by 3
- Algebra.Generators.H1Cotangent.δAux_Cstatement · cited by 3