Theorems · Theorem · ring theory

mul_boole

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

Defined in

Mathlib.Algebra.Ring.Defs

Cited by

13 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext

Assumes

MulZeroOneClassDecidable