src/HOL/Algebra/AbelCoset.thy
changeset 69220 c6b15fc78f78
parent 68975 5ce4d117cea7
child 69597 ff784d5a5bfb