src/HOL/Algebra/Coset.thy
changeset 14631 ec1e67f88f49
parent 14530 e94fd774ecf5
child 14651 02b8f3bcf7fe