Commit 2024-11-25 17:02 5c08dca6

View on Github →

feat: Finset.sup in a group (#19460)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Group/Finset.lean

added theorem Finset.add_sup''

added theorem Finset.fold_max_add

added theorem Finset.inf'_pow

added theorem Finset.mul_sup'

added theorem Finset.sup'_add'

added theorem Finset.sup'_mul

added theorem Finset.sup'_pow

added theorem Finset.sup_add_sup

Modified Mathlib/Algebra/Polynomial/Basic.lean

Modified Mathlib/Data/Finset/Fold.lean

deleted theorem Finset.fold_max_add

Modified Mathlib/Data/Finset/Lattice/Fold.lean

deleted theorem Finset.nsmul_inf'

deleted theorem Finset.nsmul_sup'

added theorem Finset.sup'_mono_fun

Modified Mathlib/Order/Filter/AtTopBot/Monoid.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean