English
For any Γ with det One, and any x ∈ ℂ, the constant function τ ↦ x defines a SlashInvariantForm Γ 0 (a weight-0 slash-invariant form).
Русский
Для любой Γ с det равным единице и любого x ∈ ℂ постоянная функция τ ↦ x задаёт SlashInvariantForm Γ 0 ( Slash-invariant форма веса 0 ).
LaTeX
$$$\forall \Gamma\ (\Gamma.HasDetOne)\ ,\forall x \in \mathbb{C},\ (\text{const}_{\Gamma,0}(x))(\tau)=x\quad\text{для всех }\tau\in\mathbb{H},\ \big(\text{const}_{\Gamma,0}(x)\big)\big|_{0}g=\text{const}_{\Gamma,0}(x)\
\text{при } g\in\Gamma,\ \det g=1.$$$
Lean4
/-- The `SlashInvariantForm` corresponding to `Function.const _ x`. -/
@[simps -fullyApplied]
def const [Γ.HasDetOne] (x : ℂ) : SlashInvariantForm Γ 0
where
toFun := Function.const _ x
slash_action_eq' g hg := by ext; simp [slash_def, σ, Subgroup.HasDetOne.det_eq hg]
