constℝ — Mathlib

English

For Γ with det plus/minus one, and x ∈ ℝ, the function τ ↦ x defines a SlashInvariantForm Γ 0.

Русский

Для Γ, удовлетворяющей условию det ±1, и x ∈ ℝ функция τ ↦ x задаёт SlashInvariantForm Γ 0.

LaTeX

$$$\forall \Gamma\ ,[Γ.HasDetPlusMinusOne]\ ,\forall x\in \mathbb{R},\ (\text{const}_{\Gamma,0}(x))(\tau)=x\quad\forall \tau\in\mathbb{H}.$$$

Lean4

/-- The `SlashInvariantForm` corresponding to `Function.const _ x`. -/
@[simps -fullyApplied]
def constℝ [Γ.HasDetPlusMinusOne] (x : ℝ) : SlashInvariantForm Γ 0
    where
  toFun := Function.const _ x
  slash_action_eq' g
    hg :=
    funext fun τ ↦ by
      simp [slash_apply, Subgroup.HasDetPlusMinusOne.abs_det hg, -Matrix.GeneralLinearGroup.val_det_apply]

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