src/HOL/Algebra/Multiplicative_Group.thy
changeset 67316 adaf279ce67b
parent 67299 ba52a058942f
child 67341 df79ef3b3a41