src/HOL/Algebra/Multiplicative_Group.thy
changeset 67497 3a0b08e7dfe9
parent 67399 eab6ce8368fa
child 68157 057d5b4ce47e