unit_mem_leftInv

Mathlib.GroupTheory.Submonoid.Inverses

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

English

If x ∈ S and x is a unit, then the inverse x^{-1} lies in S.leftInv.

Русский

Если x ∈ S и x является элементом-единицей, то x^{-1} ∈ S.leftInv.

LaTeX

$$If x ∈ S and x ∈ M^{\times}, then x^{-1} ∈ S.leftInv.$$

Lean4

@[to_additive]
theorem unit_mem_leftInv (x : Mˣ) (hx : (x : M) ∈ S) : ((x⁻¹ :) : M) ∈ S.leftInv :=
  ⟨⟨x, hx⟩, x.inv_val⟩

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

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

Разделы

Аффилиация

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