Commit 2024-11-26 14:07 13fc0e8a

View on Github →

feat(Pointwise): monotonicity of pow (#19252) ... and s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 From GrowthInGroups

Estimated changes

added theorem Finset.Nonempty.pow
added theorem Finset.Nonempty.zpow
modified theorem Finset.empty_pow
added theorem Finset.image_pow
added theorem Finset.one_mem_pow
added theorem Finset.pow_eq_empty
modified theorem Finset.pow_mem_pow
modified theorem Finset.pow_subset_pow
added theorem Finset.zpow_eq_empty
added theorem Set.Nonempty.pow
added theorem Set.Nonempty.zpow
modified theorem Set.empty_pow
added theorem Set.image_pow
added theorem Set.inter_pow_subset
added theorem Set.inv_pi
added theorem Set.one_mem_pow
added theorem Set.pow_eq_empty
modified theorem Set.pow_mem_pow
modified theorem Set.pow_subset_pow
added theorem Set.zpow_eq_empty
modified theorem egauge_zero_zero