instGroup

Mathlib.Topology.MetricSpace.DilationEquiv

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

← MathLib Explorer

English

The ratio of the inverse dilation equals the reciprocal of the ratio.

Русский

Отношение обратной дилатации равно обратному отношение.

LaTeX

$$$\operatorname{ratio}(e^{-1}) = (\operatorname{ratio}(e))^{-1}$$$

Lean4

instance : Group (X ≃ᵈ X) where
  mul e e' := e'.trans e
  mul_assoc _ _ _ := rfl
  one := refl _
  one_mul _ := rfl
  mul_one _ := rfl
  inv := symm
  inv_mul_cancel := self_trans_symm

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

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

Разделы

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

Аффилиация

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