Theorems · Theorem · ring theory

Semiring.left_distrib

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

Multiplication is left 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