Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-21 14:42 091f27e8

View on Github →

chore(order/{complete_lattice,sup_indep}): move complete_lattice.independent (#12588) Putting this here means that in future we can talk about pairwise_disjoint at the same time, which was previously defined downstream of complete_lattice.independent. This commit only moves existing declarations and adjusts module docstrings. The new authorship comes from #5971 and #7199, which predate this file.

Estimated changes