Documentation

LeanPool.LeanModularForms.Modularforms.ForMathlibSlashActions

Imports

Init
LeanPool.LeanModularForms.ForMathlib.SlashActions
Mathlib.Analysis.CStarAlgebra.Classes
Mathlib.NumberTheory.ModularForms.SlashActions

Imported by

Compatibility import for the canonical lemmas in LeanModularForms.ForMathlib.