Commit 2025-04-17 00:27 5fcae8b6
View on Github →feat: additivise Irreducible (#22904)
In the Toric project, we need to talk about (additive) irreducible elements of a lattice cone (they generate the cone). There is no definition of additive irreducible elements in mathlib, but luckily the existing definition of multiplicative irreducible elements talks about general monoids (instead of merely monoids with zero).
This PR additivises all the API, except for the parts about divisibility and monoids with zero, and moves it to a new file under Algebra.Group.
From Toric