Theorem MDifferentiable.slash

Modification history

2026-03-02 23:05

Mathlib/NumberTheory/ModularForms/Basic.lean

chore(NumberTheory/ModularForms): golf using custom elaborators (#35730) …

Modified MDifferentiable.slash View on Github →

2025-05-10 12:26

Mathlib/NumberTheory/ModularForms/Basic.lean

feat(NumberTheory/ModularForms): GL2+ action is mdifferentiable (#24573) …

Added MDifferentiable.slash View on Github →