inv_mul_mem_range_inl

Mathlib.GroupTheory.GroupExtension.Basic

URI: https://scilib.ai/kg/mathlib#GroupExtension.Section.inv_mul_mem_range_inl

← MathLib Explorer

English

The element (σ g)⁻¹ · σ' g lies in S.inl.range for any σ, σ' and g.

Русский

Элемент (σ g)⁻¹ · σ' g принадлежит S.inl.range для любых σ, σ' и g.

LaTeX

$$$ (σ g)^{-1} * σ' g \\in S.inl.range $$$

Lean4

@[to_additive]
theorem inv_mul_mem_range_inl : (σ g)⁻¹ * σ' g ∈ S.inl.range := by
  simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section, inv_mul_cancel]

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

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

Разделы

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

Аффилиация

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