seq_neg — Mathlib

English

FreeAbelianGroup carries a lawful monad structure, i.e., the monad laws hold and lift, map, pure, and bind interact as expected.

Русский

Свободная абелеева группа наделена законной монадой, т.е. выполняются законы моноида и согласованы действия lift, map, pure и bind.

LaTeX

$$$ \text{LawfulMonad}(\text{FreeAbelianGroup})$$$

Lean4

@[simp]
theorem seq_neg (f : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α) : f <*> -x = -(f <*> x) :=
  (seqAddGroupHom f).map_neg x

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