Commit 2023-12-25 02:03 de998ec5

View on Github →

chore(Algebra/Operations): golf a proof (#9201) Golf the proof of Submodule.smul_singleton and rename it to Submodule.singleton_smul.

Estimated changes

deleted theorem Submodule.smul_singleton