Mathlib Map

Theorems · Theorem · commutative algebra

Module.add_smul

∀ {R : Type u} {M : Type v} {inst : Semiring R} {inst_1 : AddCommMonoid M} [self : Module R M] (r s : R) (x : M),
  (r + s) • x = r • x + s • x

Scalar multiplication distributes over addition from the right.

Defined in
Mathlib.Algebra.Module.Defs
Cited by
1 results in Mathlib
Foundations
Depth 12 from the axioms · uses no axioms
Assumes
Module
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

add_smul · cited by 204add_smulModule · cited by 20661ModuleSemiring · cited by 13802SemiringAddCommMonoid · cited by 12281AddCommMonoidModule.add_smulCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Modulestatement and proof · cited by 20,661
  • Semiringstatement and proof · cited by 13,802
  • AddCommMonoidstatement and proof · cited by 12,281

Cited by1

Results whose statement or proof uses this declaration.