src/HOL/Algebra/FiniteProduct.thy
changeset 69766 76fbd806ebc5
parent 69313 b021008c5397
child 69895 6b03a8cf092d