src/HOL/Algebra/Multiplicative_Group.thy
changeset 77059 422c57b75b17
parent 76987 4c275405faae
child 77061 5de3772609ea