Theorems · Theorem · group theory

ite_smul

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

Defined in

Mathlib.Algebra.Group.Basic

Cited by

52 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

SMulDecidable