Commit 2026-09-11 08:52 9658bdd6

View on Github →

chore: generalize a few Type to Type* (#43704) Allow general universes for index types in some sum and product lemmas.

Estimated changes

Modified Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

modified def ModularForm.prod

modified def ModularForm.prodEqualWeights

Modified Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean

modified def SlashInvariantForm.prod

modified def SlashInvariantForm.prodEqualWeights

Modified Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean

modified theorem Filter.BoundedAtFilter.prod