src/HOL/Algebra/FiniteProduct.thy
changeset 81080 4aa4bd946f96
parent 80914 d97fdabd9e2b
child 81142 6ad2c917dd2e