src/HOL/Algebra/Multiplicative_Group.thy
changeset 69766 76fbd806ebc5
parent 69749 10e48c47a549
child 69785 9e326f6f8a24