mathlib

091f27e8 - chore(order/{complete_lattice,sup_indep}): move `complete_lattice.independent` (#12588)

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.