Commit 2025-06-03 11:40 17855c75

View on Github →

refactor(Algebra/Module/Projective): generalize universes (#24697) Generalize (P : Type max u v) to (P : Type v) [Small.{v} R] in Module.Projective.of_lifting_property and IsProjective.iff_projective. Also generalize universes in Module.Projective.iff_split.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Projective.lean

modified theorem IsProjective.iff_projective

modified theorem ModuleCat.projective_of_free

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

added theorem LinearEquiv.comp_symm

added theorem LinearEquiv.symm_comp

Modified Mathlib/Algebra/Module/Projective.lean

added theorem Module.Projective.iff_split'

modified theorem Module.Projective.of_lifting_property'

modified theorem Module.Projective.of_lifting_property

Modified Mathlib/LinearAlgebra/Finsupp/Defs.lean

added def Finsupp.mapDomain.linearEquiv