Commit 2023-05-01 17:47 8988b247

View on Github →

chore: Move lattice finset lemmas around (#3748) Match https://github.com/leanprover-community/mathlib/pull/18900

Estimated changes

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/Finset/Lattice.lean

modified theorem Finset.inf_sdiff_left

modified theorem Finset.inf_sdiff_right

modified theorem Finset.sup_sdiff_left

added theorem map_finset_inf

added theorem map_finset_sup

Modified Mathlib/LinearAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/Finsupp.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/LinearAlgebra/Quotient.lean

Modified Mathlib/Order/Hom/CompleteLattice.lean

Modified Mathlib/Order/Hom/Lattice.lean

deleted theorem map_finset_inf

deleted theorem map_finset_sup

Modified Mathlib/RingTheory/Ideal/Quotient.lean

Modified Mathlib/Topology/ContinuousOn.lean