Theorems · Theorem · group theory

dite_smul

∀ {α : Type u_1} {β : Type u_2} [inst : SMul β α] (p : Prop) [inst_1 : Decidable p] (a : α) (b : p → β) (c : ¬p → β),
  (if h : p then b h else c h) • a = if h : p then b h • a else c h • a

Defined in

Mathlib.Algebra.Group.Basic

Cited by

8 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

SMulDecidable