Commit 2025-01-02 11:03 8b781ec9

View on Github →

feat(Algebra): add missing substructure lemmas (#20269) Add missing boilerplate lemmas about the maps .toNonUnitalSubsemiring and .subsemiringClosure This PR is split off from #16094

Estimated changes