src/HOL/Algebra/Multiplicative_Group.thy
changeset 79585 dafb3d343cd6
parent 77061 5de3772609ea
child 80914 d97fdabd9e2b
equal deleted inserted replaced
79584:924e487288fb 79585:dafb3d343cd6