src/HOL/Algebra/AbelCoset.thy
changeset 81387 c677755779f5
parent 81142 6ad2c917dd2e