Monoid ideals

Stream: mathlib4

[Dexin Zhang]

A (additive) monoid ideal $I$ is a set of an additive monoid $M$ such that $\forall x\in I.\forall y\in M.x+y\in I$. Does Mathlib have a definition for that?

[Aaron Liu]

I think that would be SubAddAction Mᵃᵒᵖ M

[Aaron Liu]

docs#SubAddAction

[Aaron Liu]

the docstring say scalar multiplication though

[Aaron Liu]

I promise you it's actually the additive action

[Aaron Liu]

it's like how an ideal is a Submodule R R

[Dexin Zhang]

That's interesting! I'd also like to discuss the finiteness of a monoid ideal (like Submodule.FG), but there seems no definition of SubAddAction.FG?

[Aaron Liu]

well this is the first time I've seen a use for SubAddAction so probably no one needed it yet so it doesn't exist