lift_neg — Mathlib

English

Let α be a type and G an additive abelian group. For any function f: α → G, the lift map commutes with negation: lift(-f) = - lift f.

Русский

Пусть α — множество типов, G — абелева группа. Для любой функции f: α → G отображение lift commute с отрицанием: lift(-f) = - lift f.

LaTeX

$$$ \forall {\alpha} {G} [\operatorname{AddCommGroup} G] (f : \alpha \to G),\; \operatorname{lift}(-f) = -\,\operatorname{lift} f $$$

Lean4

@[simp]
theorem lift_neg [AddCommGroup G] (f : α → G) : lift (-f) = -lift f :=
  liftAddEquiv.map_neg f

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