src/HOL/Algebra/Coset.thy
changeset 69722 b5163b2132c5
parent 69597 ff784d5a5bfb
child 69749 10e48c47a549