Theorems · Theorem · group theory
smul_one_smul
∀ {α : Type u_5} {M : Type u_9} (N : Type u_10) [inst : Monoid N] [inst_1 : SMul M N] [inst_2 : MulAction N α]
[inst_3 : SMul M α] [IsScalarTower M N α] (x : M) (y : α), (x • 1) • y = x • y- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Monoidstatement and proof · cited by 3,887
- one_smulproof · cited by 1,374
- MulActionstatement and proof · cited by 1,294
- smul_assocproof · cited by 150
Cited by43
Results whose statement or proof uses this declaration.
- Polynomial.eval_smulproof · cited by 12
- MeasureTheory.Measure.AbsolutelyContinuous.smul_leftproof · cited by 10
- MeasureTheory.Measure.ae_smul_measureproof · cited by 10
- MeasureTheory.Measure.restrict_smulproof · cited by 8
- RCLike.real_smul_eq_coe_smulproof · cited by 5
- cfcₙ_smulproof · cited by 5
- IsScalarTower.to₁₃₄proof · cited by 5
- MeasureTheory.Measure.AbsolutelyContinuous.smulproof · cited by 4
- cfcₙ_re_idproof · cited by 4
- cfc_re_idproof · cited by 4
- cfc_smulproof · cited by 4
- Matrix.det_smul_of_towerproof · cited by 4