commensurable_inv

Mathlib.GroupTheory.Commensurable

URI: https://scilib.ai/kg/mathlib#Subgroup.Commensurable.commensurable_inv

← MathLib Explorer

English

A relationship between the commensurability of (g • H) with H and that with (g⁻¹ • H).

Русский

Связь комменсурируемости между (g • H) и H и между H и (g⁻¹ • H).

LaTeX

$$Commensurable (g • H) H ↔ Commensurable H (g⁻¹ • H)$$

Lean4

theorem commensurable_inv (H : Subgroup G) (g : ConjAct G) : Commensurable (g • H) H ↔ Commensurable H (g⁻¹ • H) := by
  rw [commensurable_conj, inv_smul_smul]

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

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

Разделы

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

Аффилиация

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