Theorems · Theorem · ring theory

boole_mul

∀ {α : Type u_1} [inst : MulZeroOneClass α] (P : Prop) [inst_1 : Decidable P] (a : α),
  (if P then 1 else 0) * a = if P then a else 0

Defined in

Mathlib.Algebra.Ring.Defs

Cited by

3 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext

Assumes

MulZeroOneClassDecidable