src/HOL/Algebra/FiniteProduct.thy
changeset 60597 2da9b632069b
parent 60112 3eab4acaa035
child 60773 d09c66a0ea10