leftInv_leftInv_le

Mathlib.GroupTheory.Submonoid.Inverses

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

← MathLib Explorer

English

For any submonoid S of M, S.leftInv.leftInv ≤ S.

Русский

Для любого подмономоида S в M, S.leftInv.leftInv ⊆ S.

LaTeX

$$S.leftInv.leftInv ≤ S$$

Lean4

@[to_additive]
theorem leftInv_leftInv_le : S.leftInv.leftInv ≤ S :=
  by
  rintro x ⟨⟨y, z, h₁⟩, h₂ : x * y = 1⟩
  convert z.prop
  rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]

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

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

Разделы

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

Аффилиация

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