Commit 2025-09-17 21:07 6a4c8968

View on Github →

feat(Grp_): η ≫ ι = η (#29736) and another simple lemma. From Toric

Estimated changes

added theorem GrpObj.one_inv
added theorem Grp_.homMk_hom'