Commit 2025-02-28 22:16 65e3445a

View on Github →

feat(Pointwise): add smul_set_prod and smul_set_pi (#22029)

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

added theorem Set.smul_set_pi_of_surjective

added theorem Set.smul_set_univ_pi

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

added theorem Set.smul_set_pi

added theorem Set.smul_set_pi_of_isUnit

added theorem Set.smul_set_pi₀

added theorem Set.smul_set_prod