src/HOL/Algebra/FiniteProduct.thy
changeset 46681 c083a3f621c0
parent 44890 22f665a2e91c
child 46721 f88b187ad8ca