copy — Mathlib

English

Copy of a SlashInvariantForm with a new toFun equal to the old one; preserves the slash-action structure.

Русский

Копия SlashInvariantForm с новым toFun, равным старому; сохраняет структуру slash-действия.

LaTeX

$$$\text{copy}(f, f', h) : SlashInvariantForm Γ k$ with toFun := f' and slash_action_eq' := h.symm ▸ f.slash_action_eq'$$

Lean4

/-- Copy of a `SlashInvariantForm` with a new `toFun` equal to the old one.
Useful to fix definitional equalities. -/
protected def copy (f : SlashInvariantForm Γ k) (f' : ℍ → ℂ) (h : f' = ⇑f) : SlashInvariantForm Γ k
    where
  toFun := f'
  slash_action_eq' := h.symm ▸ f.slash_action_eq'

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