Commit 2023-04-01 11:24 3b6fdff1

View on Github →

feat: When s ×ˢ t is finite (#3214) Match https://github.com/leanprover-community/mathlib/pull/18674

Estimated changes

Modified Mathlib/Data/Set/Finite.lean

deleted theorem Set.Finite.image2

added theorem Set.Finite.of_prod_left

added theorem Set.Finite.of_prod_right

deleted theorem Set.Finite.offDiag

deleted theorem Set.Finite.prod

deleted theorem Set.Infinite.nonempty

added theorem Set.Infinite.of_image

added theorem Set.finite_prod

added theorem Set.infinite_image2

deleted theorem Set.infinite_of_infinite_image

Modified Mathlib/Data/Set/Pointwise/Finite.lean

added theorem Set.Infinite.of_smul_set

added theorem Set.finite_smul_set

added theorem Set.infinite_mul

added theorem Set.infinite_smul_set