inv_mk

Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

URI: https://scilib.ai/kg/mathlib#Algebra.GrothendieckGroup.inv_mk

English

For any m ∈ M and s ∈ ⊤, the inverse of mk m s is mk s ⟨m, mem_top⟩.

Русский

Для любого m ∈ M и s ∈ ⊤ обратное к mk m s равно mk s ⟨m, mem_top⟩.

LaTeX

$$$(\\mathrm{mk}\,m\\,s)^{-1} = \\mathrm{mk}\\,s\\langle m, \\mathrm{mem\\_top}\\ rangle$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_mk (m : M) (s : (⊤ : Submonoid M)) : (mk m s)⁻¹ = .mk s ⟨m, Submonoid.mem_top _⟩ :=
  rfl

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

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

Разделы

Аффилиация

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