funLike — Mathlib

English

SlashInvariantForm is equipped with a FunLike structure: there is a canonical function coercion to functions ℍ → ℂ and equality is determined by underlying functions.

Русский

SlashInvariantForm снабжен структурой FunLike: есть каноническое отображение в функции ℍ → ℂ и равенство форм определяется по значениям функций.

LaTeX

$$$\text{SlashInvariantForm}.toFun = (\text{SlashInvariantForm} \,\text{as function})$$$

Lean4

instance (priority := 100) funLike : FunLike (SlashInvariantForm Γ k) ℍ ℂ
    where
  coe := SlashInvariantForm.toFun
  coe_injective' f g h := by cases f; cases g; congr

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