Commit 2026-02-03 04:16 58a8e4ff

View on Github →

chore(RingTheory): clean up code (#34360) Utilise opened namespaces where available, spell out projections, style, shorten proofs. No new definitions/theorems.

Estimated changes

modified theorem Module.Finite.iff_fg
modified theorem Module.Finite.exists_fin
modified theorem Submodule.fg_def