Commit 2025-01-10 22:02 013b3e65

View on Github →

chore: initialize_simps_projections for Submodule (#20582) From GrowthInGroups (LeanCamCombi)

Estimated changes

deleted theorem Submodule.coe_copy