Theorems · Theorem

ite_mul

∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Mul α] (a b c : α),
  (if P then a else b) * c = if P then a * c else b * c

Defined in

Mathlib.Algebra.Notation.Defs

Cited by

83 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

DecidableMul