Theorems · Theorem · group theory

ite_pow

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

Defined in

Mathlib.Algebra.Group.Basic

Cited by

10 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

PowDecidable