coe_zero — Mathlib

English

There is a zero element in SlashInvariantForm Γ k given by the zero function, which is invariant under slash action.

Русский

Существует нулевой элемент в SlashInvariantForm Γ k, задаваемый нулевой функцией, сохраняющей слэш-акцию.

LaTeX

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

Lean4

@[simp]
theorem coe_zero : ⇑(0 : SlashInvariantForm Γ k) = (0 : ℍ → ℂ) :=
  rfl

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