Commit 2024-05-30 14:45 fdaf1756

View on Github →

chore: Do not import algebra in Data.Finset.Lattice (#13243) Move the OrderBot Nat instance to a new file Order.Nat and the LinearOrderedSemiring lemmas from Data.Finset.Lattice to a new file Algebra.Order.Ring.Finset. I credit Eric for https://github.com/leanprover-community/mathlib/pull/12912.

Estimated changes

Modified Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Basic.lean

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/Order/Group/Nat.lean

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

added theorem Finset.inf'_mul_le_mul_inf'_of_nonneg

added theorem Finset.mul_inf_le_inf_mul_of_nonneg

added theorem Finset.sup'_mul_le_mul_sup'_of_nonneg

added theorem Finset.sup_mul_le_mul_sup_of_nonneg

Modified Mathlib/Analysis/Normed/Field/Basic.lean

Modified Mathlib/Combinatorics/Additive/FreimanHom.lean

Modified Mathlib/Combinatorics/Hall/Finite.lean

Modified Mathlib/Combinatorics/SetFamily/Shatter.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

Modified Mathlib/Data/Finset/Fold.lean

Modified Mathlib/Data/Finset/Lattice.lean

deleted theorem Finset.inf'_mul_le_mul_inf'_of_nonneg

deleted theorem Finset.mul_inf_le_inf_mul_of_nonneg

deleted theorem Finset.sup'_mul_le_mul_sup'_of_nonneg

deleted theorem Finset.sup_mul_le_mul_sup_of_nonneg

Modified Mathlib/Data/Finset/NatAntidiagonal.lean

Modified Mathlib/Data/Finset/Sups.lean

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/List/ToFinsupp.lean

Modified Mathlib/Data/Multiset/Fintype.lean

modified theorem Multiset.coe_mem

Modified Mathlib/Data/Nat/Defs.lean

Modified Mathlib/Data/Nat/Lattice.lean

Modified Mathlib/Data/Set/Finite.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Interval/Finset/Basic.lean

Modified Mathlib/Order/Interval/Finset/Fin.lean

Modified Mathlib/Order/Interval/Finset/Nat.lean

modified theorem Nat.Ico_zero_eq_range

modified theorem Nat.card_Iic

modified theorem Nat.card_Iio

modified theorem Nat.card_uIcc

Created Mathlib/Order/Nat.lean

Modified Mathlib/RingTheory/Nilpotent/Defs.lean

Modified Mathlib/Tactic/RewriteSearch.lean