src/HOL/Algebra/Multiplicative_Group.thy
changeset 67087 733017b19de9
parent 67051 e7e54a0b9197
child 67226 ec32cdaab97b