ite_pow

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#ite_pow

← MathLib Explorer

English

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

Русский

Пусть p — произвольное высказывание; тогда (ite(p,a,b))^c = ite(p, a^c, b^c).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru