Theorems · Inductive type · group theory
DistribSMul
Type u_12 → (A : Type u_13) → [AddZeroClass A] → Type (max u_12 u_13)
Typeclass for scalar multiplication that preserves 0 and + on the right.
This is exactly DistribMulAction without the MulAction part.
- Cited by
- 117 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- AddZeroClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddZeroClassstatement · cited by 1,237
Cited by147
Results whose statement or proof uses this declaration.
- smul_addstatement and proof · cited by 263
- smul_negstatement and proof · cited by 181
- smul_substatement and proof · cited by 142
- Finset.smul_sumstatement and proof · cited by 88
- DistribSMul.toLinearMapstatement and proof · cited by 50
- DistribSMul.toAddMonoidHomstatement and proof · cited by 20
- DistribSMul.toLinearMap_applystatement and proof · cited by 18
- LinearMap.smul_applystatement and proof · cited by 15
- Finsupp.smul_sumstatement and proof · cited by 11
- AddSubmonoid.smulstatement and proof · cited by 11
- HasSum.const_smulstatement and proof · cited by 11
- AffineSubspace.pointwiseSMulstatement and proof · cited by 9