ratio_pow

Mathlib.Topology.MetricSpace.Dilation

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

English

Raising a dilation to the nth power scales the ratio by the nth power: ratio(f^n) = (ratio f)^n.

Русский

Возведение дилатации в степень n масштабирует отношение в степени n: ratio(f^n) = (ratio f)^n.

LaTeX

$$$\\operatorname{ratio}(f^{n}) = (\\operatorname{ratio}(f))^{n}$$$

Lean4

@[simp]
theorem ratio_pow (f : α →ᵈ α) (n : ℕ) : ratio (f ^ n) = ratio f ^ n :=
  ratioHom.map_pow _ _

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

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

Разделы

Аффилиация

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