ratio_pow

Mathlib.Topology.MetricSpace.DilationEquiv

URI: https://scilib.ai/kg/mathlib#DilationEquiv.ratio_pow

English

The ratio respects integer powers: ratio(e^n) = (ratio e)^n for integers n.

Русский

ratio сохраняет целочисленные степени: ratio(e^n) = (ratio e)^n для целых n.

LaTeX

$$$\forall e : X \simeq^{\mathrm{d}} X,\ \forall n \in \mathbb{Z},\ \operatorname{ratio}(e^n) = (\operatorname{ratio}(e))^n$$$

Lean4

@[simp]
theorem ratio_pow (e : X ≃ᵈ X) (n : ℕ) : ratio (e ^ n) = ratio e ^ n :=
  ratioHom.map_pow _ _

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

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

Разделы

Аффилиация

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