coe_add — Mathlib

English

The underlying function of the sum of two slash-invariant forms is the pointwise sum of their underlying functions.

Русский

Функция, соответствующая сумме двух slash-инвариантных форм, равна попарной сумме их соответствующих функций.

LaTeX

$$$$ (f+g)(z) = f(z) + g(z) \quad\\text{for all } z \\in \\mathbb{H}. $$$$

Lean4

@[simp]
theorem coe_add (f g : SlashInvariantForm Γ k) : ⇑(f + g) = f + g :=
  rfl

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