Independent iff independent

Stream: Is there code for X?

[Adam Topaz]

Do we have the following example?
https://github.com/leanprover-community/mathlib/blob/980185a1a2ecb4d21445f2407b22044b56b5cd00/src/order/sup_indep.lean#L205

[Yaël Dillies]

That should be more or less by definition

[Eric Wieser]

You're looking for a statement along the lines of linear_independent R v ↔ complete_lattice.independent (λ i, span R {v I}), right?

[Eric Wieser]

I'm pretty sure I've at least seen one direction of that