Commit 2025-06-22 15:35 50a12a26

View on Github →

refactor: split BooleanAlgebra into Basic and Defs (#26173) To avoid import loops, splits BooleanAlgebra into BooleanAlgebra.Defs and BooleanAlgebra.Basic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Ring/Idempotent.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/SymmDiff.lean

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

deleted theorem Bool.compl_eq_bnot

deleted theorem Bool.inf_eq_band

deleted theorem Bool.sup_eq_bor

deleted def DistribLattice.booleanAlgebraOfComplemented

Created Mathlib/Order/BooleanAlgebra/Defs.lean

added theorem Bool.compl_eq_bnot

added theorem Bool.inf_eq_band

added theorem Bool.sup_eq_bor

added def DistribLattice.booleanAlgebraOfComplemented

Modified Mathlib/Order/Booleanisation.lean

Modified Mathlib/Order/Heyting/Boundary.lean

Modified Mathlib/Order/SymmDiff.lean