src/HOL/Algebra/Multiplicative_Group.thy
changeset 69766 76fbd806ebc5
parent 69749 10e48c47a549
child 69785 9e326f6f8a24
equal deleted inserted replaced
69765:c5778547ed03 69766:76fbd806ebc5