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, AddMonoid.FG M, IsAddTorsionFree 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
• fg_top : ⊤.FG
• 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, Monoid.FG M, IsMulTorsionFree 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
• fg_top : ⊤.FG
• pow_left_injective ⦃n : ℕ⦄ (hn : n ≠ 0) : Function.Injective fun (a : M) => a ^ n