Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-30 23:39 7080d596

View on Github →

feat(combinatorics/additive/energy): Additive energy (#17734) Define the additive energy of two finsets in a group.

Estimated changes

Created src/combinatorics/additive/energy.lean

added theorem finset.le_multiplicative_energy

added def finset.multiplicative_energy

added theorem finset.multiplicative_energy_comm

added theorem finset.multiplicative_energy_empty_left

added theorem finset.multiplicative_energy_empty_right

added theorem finset.multiplicative_energy_eq_zero_iff

added theorem finset.multiplicative_energy_mono

added theorem finset.multiplicative_energy_mono_left

added theorem finset.multiplicative_energy_mono_right

added theorem finset.multiplicative_energy_pos

added theorem finset.multiplicative_energy_pos_iff

added theorem finset.multiplicative_energy_univ_left

added theorem finset.multiplicative_energy_univ_right

Modified src/order/basic.lean

added theorem has_le.le.ge_iff_eq

added theorem has_le.le.gt_iff_ne

modified theorem has_le.le.le_iff_eq

modified theorem has_le.le.lt_iff_ne

added theorem has_le.le.not_gt_iff_eq

added theorem has_le.le.not_lt_iff_eq