quot_map_mk

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.quot_map_mk

← MathLib Explorer

English

Quot.map f H (mk L) = mk (f L) for f commuting with Red.Step.

Русский

Quot.map f H (mk L) = mk (f L) при условии, что f согласуется со Red.Step.

LaTeX

$$$\operatorname{Quot.map} f H (\mathrm{mk}(L)) = \mathrm{mk}(f(L)).$$$

Lean4

@[to_additive (attr := simp)]
theorem quot_map_mk (β : Type v) (f : List (α × Bool) → List (β × Bool)) (H : (Red.Step ⇒ Red.Step) f f) :
    Quot.map f H (mk L) = mk (f L) :=
  rfl

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

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

Разделы

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

Аффилиация

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