Commit 2020-10-14 09:45 6f5ccc1e

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;