Theorems · Theorem · group theory
smul_one_mul
∀ {M : Type u_9} {N : Type u_10} [inst : MulOneClass N] [inst_1 : SMul M N] [IsScalarTower M N N] (x : M) (y : N),
x • 1 * y = x • y- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- MulOneClassSMulIsScalarTower
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- one_mulproof · cited by 2,841
- MulOneClassstatement and proof · cited by 1,018
- smul_mul_assocproof · cited by 77
Cited by15
Results whose statement or proof uses this declaration.
- Polynomial.eval_smulproof · cited by 12
- ENNReal.smul_topproof · cited by 3
- MeasureTheory.Measure.prod_smul_rightproof · cited by 3
- ENNReal.smul_iSupproof · cited by 2
- NumberField.mixedEmbedding.logMap_real_smulproof · cited by 2
- bernsteinPolynomial.sum_mul_smulproof · cited by 1
- ENat.smul_iSupproof · cited by 1
- Polynomial.nnqsmul_eq_C_mulproof · cited by 0
- Module.IsTorsionFree.transproof · cited by 0
- ENNReal.smul_sSupproof · cited by 0
- ENNReal.tsum_const_smulproof · cited by 0
- Polynomial.eval₂_smulOneHom_eq_smevalproof · cited by 0