pow_ite — Mathlib

English

For any p, and a ∈ α, b, c ∈ β, a^{ite(p,b,c)} = ite(p, a^b, a^c).

Русский

Пусть p — произвольное высказывание; тогда для любых a ∈ α, b,c ∈ β верно: a^{ite(p,b,c)} = ite(p, a^b, a^c).

LaTeX

$$$a^{\mathrm{ite}(p,b,c)} = \mathrm{ite}(p, a^{b}, a^{c})$$$

Lean4

@[to_additive (attr := simp) ite_smul]
theorem pow_ite (p : Prop) [Decidable p] (a : α) (b c : β) : a ^ (if p then b else c) = if p then a ^ b else a ^ c :=
  pow_dite _ _ _ _

Похожие утверждения