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
feat(Algebra): add missing substructure lemmas (#20269)
Add missing boilerplate lemmas about the maps .toNonUnitalSubsemiring
and .subsemiringClosure
This PR is split off from #16094