Yama2026_Sections_1_And_2_1
This module formalizes Section 1 and Subsection 2.1 of Yamaguchi's paper on center-freeness.
main
The additive automorphism of the coset-function module obtained by reindexing cosets along the left action of a group element.