coe_pow

Mathlib.Analysis.Normed.Field.UnitBall

URI: https://scilib.ai/kg/mathlib#Metric.unitClosedBall.coe_pow

← MathLib Explorer

English

For x in the closed unit ball and n a natural number, the coercion commutes with the power: ↑(x^n) = (x)^n.

Русский

Для x в замкнутом шаре единицы и натурального n выполнено: ↑(x^n) = (x)^n.

LaTeX

$$$↑(x^n) = x^n$$$

Lean4

@[simp, norm_cast]
protected theorem coe_pow [SeminormedRing 𝕜] [NormOneClass 𝕜] (x : closedBall (0 : 𝕜) 1) (n : ℕ) :
    ↑(x ^ n) = (x : 𝕜) ^ n :=
  rfl

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

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

Разделы

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

Аффилиация

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