chore(linear_algebra/linear_independent): review API (#4567)
### API changes
#### New definitions and lemmas
* `subalgebra.to_submodule_equiv`: a linear equivalence between a subalgebra and its coercion
to a submodule;
* `algebra.to_submodule_bot`: coercion of `⊥ : subalgebra R A` to `submodule R A` is
`submodule.span {1}`;
* `submodule.disjoint_def'`: one more expansion of `disjoint` for submodules;
* `submodule.is_compl_range_inl_inr`: ranges of `inl` and `inr` are complement submodules;
* `finsupp.supported_inter`, `finsupp.disjojint_supported_supported`,
`finsupp.disjoint_supported_supported_iff` : more lemmas about `finsupp.supported`;
* `finsupp.total_unique`: formula for `finsupp.total` on a `unique` type;
* `linear_independent_iff_injective_total`, `linear_independent.injective_total` :
relate `linear_independent R v` to `injective (finsupp.total ι M R v)`;
* `fintype.linear_independent_iff`: a simplified test for
`linear_independent R v` if the domain of `v` is a `fintype`;
* `linear_independent.map'`: an injective linear map sends linearly
independent families of vectors to linearly independent families of
vectors;
* `linear_map.linear_independent_iff`: if `f` is an injective linear
map, then `f ∘ v` is linearly independent iff `v` is linearly
independent;
* `linear_independent.disjoint_span_image`: if `v` is a linearly
independent family of vectors, then the submodules spanned by
disjoint subfamilies of `v` are disjoint;
* `linear_independent_sum`: a test for linear independence of a
disjoint union of two families of vectors;
* `linear_independent.sum_type`: `iff.mpr` from `linear_independent_sum`;
* `linear_independent_unique_iff`, `linear_independent_unique`: a test
for linear independence of a single-vector family;
* `linear_independent_option'`, `linear_independent_option`, `linear_independent.option`:
test for linear independence of a family indexed by `option ι`;
* `linear_independent_pair`: test for independence of `{v₁, v₂}`;
* `linear_independent_fin_cons`, `linear_independent.fin_cons`,
`linear_independent_fin_succ`, `linear_independent_fin2`: tests for
linear independence of families indexed by `i : fin n`.
#### Rename
* `_root_.disjoint_span_singleton` → `submodule.disjoint_span_singleton'`;
* `linear_independent.image` → `linear_independent.map`
* `linear_independent_of_comp` → `linear_independent.of_comp`;
#### Changes in type signature
* `is_basis.to_dual`, `is_basis.to_dual_flip`, `is_basis.to_dual_equiv`: take `B` as an explicit
argument to improve readability of the pretty-printed output;
