src/HOL/Algebra/Multiplicative_Group.thy
changeset 73011 4519ba8da368
parent 72630 4167d3d3d478
child 73102 87067698ae53