Commit 2025-09-01 13:46 1843f443

View on Github →

fix: generalize indexed lattice lemmas to Sort (#29189)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

modified theorem Subgroup.normal_iInf_normal

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

modified theorem Submodule.inf_iInf

Modified Mathlib/Algebra/Module/Submodule/Map.lean

modified theorem Submodule.map_iInf