fromLeftInv_eq_inv

Mathlib.GroupTheory.Submonoid.Inverses

URI: https://scilib.ai/kg/mathlib#Submonoid.fromLeftInv_eq_inv

← MathLib Explorer

English

For x ∈ S.leftInv, the image under fromLeftInv is the inverse of x in M: (S.fromLeftInv x : M) = (x : M)^{-1}.

Русский

Для x ∈ S.leftInv образ fromLeftInv x равен обратному x в M.

LaTeX

$$$ (S.fromLeftInv x : M) = (x : M)^{-1} $$$

Lean4

@[to_additive (attr := simp)]
theorem fromLeftInv_eq_inv (x : S.leftInv) : (S.fromLeftInv x : M) = (x : M)⁻¹ := by
  rw [← mul_right_inj (x : M), mul_inv_cancel, mul_fromLeftInv]

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

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

Разделы

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

Аффилиация

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