Formalization of Augmentation map

Stream: mathlib4

[Kitsune Kiriha]

Is the correct formulation of the augmentation map for a group ring (MonoidAlgebra) in Mathlib4 MonoidAlgebra.lift k G k 1? I've not found any more intuitive ways to express this.

[Antoine Chambert-Loir]

Yes it is. Maybe the only thing that could help to be clarify this notation is that the final 1 has type G →* k, that is, is a monoid homomorphism from G to k (the multiplicative monoid of the commutative semiring k), and is provided by the instance docs#instOneMonoidHom.