Commit 2024-02-01 18:57 e64d0a16

View on Github →

refactor(Order/CompleteLatticeIntervals): move lemmas with a multiset dependency to a new file (#10165) This reworks the location of the lemmas from #10086, by moving them to a new Mathlib.Order.CompactlyGenerated.Intervals file. The existing Mathlib.Order.CompactlyGenerated is moved to Mathlib.Order.CompactlyGenerated.Basic for consistency.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Span.lean

Renamed Mathlib/Order/CompactlyGenerated.lean to Mathlib/Order/CompactlyGenerated/Basic.lean

Created Mathlib/Order/CompactlyGenerated/Intervals.lean

added theorem Set.Iic.isCompactElement

added theorem complementedLattice_of_complementedLattice_Iic

Modified Mathlib/Order/CompleteLatticeIntervals.lean

deleted theorem Set.Iic.isCompactElement

deleted theorem complementedLattice_of_complementedLattice_Iic

Modified Mathlib/RingTheory/SimpleModule.lean

Modified Mathlib/Topology/Sets/Opens.lean