Mathlib Map

Theorems · Theorem · ring theory

Distrib.left_distrib

∀ {R : Type u_1} [self : Distrib R] (a b c : R), a * (b + c) = a * b + a * c

Multiplication is left distributive over addition

Defined in
Mathlib.Algebra.Ring.Defs
Cited by
0 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
Distrib
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Function.Injective.nonUnitalNonAssocSemiring · cited by 0Injective.nonUnitalNonAss…Function.Surjective.nonUnitalNonAssocSemiring · cited by 0Surjective.nonUnitalNonAs…Distrib · cited by 31DistribDistrib.left_distribCITED BYCITES

Cites1

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

  • Distribstatement and proof · cited by 31

Cited by2

Results whose statement or proof uses this declaration.