map_comp

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Submonoid.LocalizationMap.map_comp

← MathLib Explorer

English

Behavior on localized generators.

Русский

Поведение на локализуемых генераторах.

LaTeX

$$$ f.map\\ hy\\ k (f.mk'(x,y)) = k.mk'(g x) \\langle g y, hy y \\rangle $$$

Lean4

@[to_additive (attr := simp)]
theorem map_comp : (f.map hy k).comp f.toMonoidHom = k.toMonoidHom.comp g :=
  f.lift_comp fun y ↦ k.map_units ⟨g y, hy y⟩

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

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

Разделы

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

Аффилиация

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