lift_mk'_spec

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Submonoid.LocalizationMap.lift_mk'_spec

← MathLib Explorer

English

For all x ∈ M and y ∈ S, f.lift hg (f.mk' x y) equals g x times inverse of g y.

Русский

Для всех x ∈ M и y ∈ S, f.lift hg (f.mk' x y) = g x (g y)^{-1}.

LaTeX

$$$ f.lift hg (f.mk' x y) = g x \cdot (g y)^{-1} $$$

Lean4

@[to_additive]
theorem lift_mk'_spec (x v) (y : S) : f.lift hg (f.mk' x y) = v ↔ g x = g y * v := by rw [f.lift_mk' hg];
  exact mul_inv_left hg _ _ _

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

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

Разделы

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

Аффилиация

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