Commit 2021-04-21 19:58 721e0b9e

feat(order/complete_lattice): independence of an indexed family (#7199) This PR reclaims the concept of independent for elements of a complete lattice. Right now it's defined on subsets -- a subset of a complete lattice L is independent if every element of it is disjoint from (i.e. bot is the meet of it with) the Sup of all the other elements. The problem with this is that if you have an indexed family f:I->L of elements of L then duplications get lost if you ask for the image of f to be independent (rather like the issue with a basis of a vector space being a subset rather than an indexed family). This is an issue when defining gradings on rings, for example: if M is a monoid and R is a ring, then I don't want the map which sends every m to (top : subgroup R) to be independent. I have renamed the set-theoretic version of independent to set_independent