Mathlib Map

Theorems · Theorem · ring theory

Semiring.right_distrib

∀ {α : Type u} [self : Semiring α] (a b c : α), (a + b) * c = a * c + b * c

Multiplication is right distributive over addition

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

Around this declaration

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

Semiring.ext · cited by 5Semiring.extCommCStarAlgebra.toStarRing · cited by 2CommCStarAlgebra.toStarRi…CStarAlgebra.mk.noConfusion · cited by 0mk.noConfusionCStarAlgebra.casesOn · cited by 0CStarAlgebra.casesOnCommCStarAlgebra.casesOn · cited by 0CommCStarAlgebra.casesOnRCLike.casesOn · cited by 0RCLike.casesOnCommCStarAlgebra.recOn · cited by 0CommCStarAlgebra.recOnRCLike.recOn · cited by 0RCLike.recOnCommCStarAlgebra.mk.noConfusion · cited by 0mk.noConfusionCStarAlgebra.recOn · cited by 0CStarAlgebra.recOnRCLike.mk.noConfusion · cited by 0mk.noConfusionCommCStarAlgebra.toStarModule · cited by 0CommCStarAlgebra.toStarMo…Semiring · cited by 13802SemiringSemiring.right_distribCITED BYCITES

Cites1

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

  • Semiringstatement and proof · cited by 13,802

Cited by12

Results whose statement or proof uses this declaration.