src/HOL/Algebra/Multiplicative_Group.thy
changeset 66787 64b47495676d
parent 66500 ba94aeb02fbc
child 67051 e7e54a0b9197