mulSingle_inv

Mathlib.Algebra.Group.Pi.Lemmas

URI: https://scilib.ai/kg/mathlib#Pi.mulSingle_inv

← MathLib Explorer

English

For all i, x ∈ f i, mulSingle i x⁻¹ = (mulSingle i x)⁻¹.

Русский

Пусть i ∈ I, x ∈ f i. Тогда mulSingle i x^{-1} = (mulSingle i x)^{-1}.

LaTeX

$$$ \mathrm{mulSingle} \ i x^{-1} = (\mathrm{mulSingle} \ i x)^{-1} $$$

Lean4

@[to_additive]
theorem mulSingle_inv [∀ i, Group <| f i] (i : I) (x : f i) : mulSingle i x⁻¹ = (mulSingle i x)⁻¹ :=
  (MonoidHom.mulSingle f i).map_inv x

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

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

Разделы

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

Аффилиация

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