lift_eq_prod_map — Mathlib

English

For any β with a group structure and any f: α → β, the lifting of f equals the map on words followed by prod.

Русский

Для любого β с групповой структурой и любого f: α → β, подъём f равен отображению на словах далее prod.

LaTeX

$$$ lift\\ f = prod \\circ map\\ f $$$

Lean4

@[to_additive]
theorem lift_eq_prod_map {β : Type v} [Group β] {f : α → β} {x} : lift f x = prod (map f x) := by
  rw [← lift_unique (prod.comp (map f)) (by simp), MonoidHom.coe_comp, Function.comp_apply]

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