src/HOL/Algebra/Coset.thy
changeset 81577 a712bf5ccab0
parent 81438 95c9af7483b1
child 82248 e8c96013ea8a