Commit 2024-07-21 23:44 a5fb11c5

View on Github →

feat (Algebra/Order/AddTorsor) : Antidiagonals for SMul and VAdd, with finiteness properties (#14479) We introduce antidiagonals for scalar multiplication and vector addition, and show that they are finite for partially well-ordered input sets. We also add some results involving minima. This will be used in future PRs on Hahn modules and vertex operators.

depends on: #14732

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/AddTorsor.lean

added theorem IsOrderedSMul.smul_le_smul

added theorem Monotone.smul

Created Mathlib/Data/Finset/SMulAntidiagonal.lean

added theorem Finset.SMulAntidiagonal_min_smul_min

added theorem Finset.isPWO_support_smulAntidiagonal

added theorem Finset.mem_smulAntidiagonal

added theorem Finset.smulAntidiagonal_mono_left

added theorem Finset.smulAntidiagonal_mono_right

added theorem Finset.support_smulAntidiagonal_subset_smul

added theorem Set.IsPWO.smul

added theorem Set.IsWF.min_smul

added theorem Set.IsWF.smul

Created Mathlib/Data/Set/SMulAntidiagonal.lean

added theorem Set.SMulAntidiagonal.eq_of_fst_eq_fst

added theorem Set.SMulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd

added theorem Set.SMulAntidiagonal.eq_of_snd_eq_snd

added theorem Set.SMulAntidiagonal.finite_of_isPWO

added theorem Set.SMulAntidiagonal.fst_eq_fst_iff_snd_eq_snd

added theorem Set.mem_smulAntidiagonal

added def Set.smulAntidiagonal

added theorem Set.smulAntidiagonal_mono_left

added theorem Set.smulAntidiagonal_mono_right