Commit 2025-01-06 11:22 e58d5d72
View on Github →chore(RingTheory/Finiteness): rename Module.Finite.out (#20506) Right now it's impossible to do
-- finite projective modules
class IsFiniteProjective extends Module.Projective R M, Module.Finite R M : Prop where -- oops
because of a nameclash (both axioms are called out).