ratio_zpow

Mathlib.Topology.MetricSpace.DilationEquiv

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

English

Further ratio rules for integer powers of DilationEquiv.

Русский

Дополнительные правила ratio для целочисленных степеней дилатационных эквивалентностей.

LaTeX

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

Lean4

@[simp]
theorem ratio_zpow (e : X ≃ᵈ X) (n : ℤ) : ratio (e ^ n) = ratio e ^ n :=
  ratioHom.map_zpow _ _

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

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

Разделы

Аффилиация

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