Affine monoids

This file defines affine monoids as finitely generated cancellative torsion-free commutative monoids.

class IsAffineAddMonoid (M : Type u_1) [AddCommMonoid M] extends IsCancelAdd M, IsAddFG M, HasUniqueDiv M : Prop

An affine monoid is a finitely generated cancellative torsion-free commutative monoid.

• add_left_cancel (a : M) : IsAddLeftRegular a
• add_right_cancel (a : M) : IsAddRightRegular a
• out : ∃ (S : Finset M), AddSubsemigroup.closure ↑S = ⊤
• nsmul_right_injective ⦃n : ℕ⦄ (hn : n ≠ 0) : Function.Injective fun (a : M) => n • a

class IsAffineMonoid (M : Type u_1) [CommMonoid M] extends IsCancelMul M, IsMulFG M, HasUniqueRoots M : Prop

An affine monoid is a finitely generated cancellative torsion-free commutative monoid.

• mul_left_cancel (a : M) : IsLeftRegular a
• mul_right_cancel (a : M) : IsRightRegular a
• out : ∃ (S : Finset M), Subsemigroup.closure ↑S = ⊤
• pow_left_injective ⦃n : ℕ⦄ (hn : n ≠ 0) : Function.Injective fun (a : M) => a ^ n