src/HOL/Algebra/Left_Coset.thy
changeset 77820 15edec78869c
parent 77089 b4f892d0625d
child 80914 d97fdabd9e2b