Commit 2025-04-01 19:01 1e7f890b
View on Github →refactor: generalise ∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1 to monoids with a single unit (#23483)
namely whose only unit is 1. Also unprime the multiplicative name since it doesn't conflict with anything.
From Toric