Theorems · Theorem

dite_mul

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

Defined in

Mathlib.Algebra.Notation.Defs

Cited by

6 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

DecidableMul