Commit 2024-10-22 16:44 ddeafa99

View on Github →

feat(Pointwise): growth of finsets (#18003) This PR proves the monotonicity of n ↦ s ^ n under various conditions. Also rename empty_nsmul to nsmul_empty. From GrowthInGroups

Estimated changes

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

added theorem Finset.card_le_card_pow

added theorem Finset.card_pow_le

added theorem Finset.card_pow_mono

added theorem Finset.empty_zpow

added theorem Finset.singleton_pow

added theorem Finset.singleton_zpow

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

added theorem Set.empty_zpow

added theorem Set.singleton_pow

added theorem Set.singleton_zpow