Commit 2024-02-13 21:51 9b6ad3c9
View on Github →feat: Submonoid of nonnegative elements (#10209)
Define the Submonoid of elements greater than 1, the AddSubmonoid of nonnegative elements, move posSubmonoid with them and rename it to Submonoid.pos.
From LeanAPAP and partly extracted from #4871