instNeg — Mathlib

English

There is a negation on SlashInvariantForm Γ k, given by f ↦ -f, and it commutes with the slash action.

Русский

Существует операция отрицания на SlashInvariantForm Γ k: f ↦ -f, которая сохраняет слэш-акцию.

LaTeX

$$$$ (-f)(\\gamma \\cdot z) = -\\bigl(f(\\gamma \\cdot z)\\bigr). $$$$

Lean4

instance instNeg : Neg (SlashInvariantForm Γ k) :=
  ⟨fun f =>
    { toFun := -f
      slash_action_eq' := fun γ hγ => by rw [SlashAction.neg_slash, slash_action_eqn f γ hγ] }⟩

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