Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-14 11:14 3da777aa

View on Github →

chore(linear_algebra/basis): use dot notation, simplify some proofs (#2671)

Estimated changes

Modified src/analysis/normed_space/finite_dimension.lean

modified theorem continuous_equiv_fun_basis

added theorem continuous_linear_map.exists_right_inverse_of_surjective

Modified src/linear_algebra/basis.lean

modified theorem constr_basis

modified theorem exists_is_basis

deleted theorem exists_left_inverse_linear_map_of_injective

deleted theorem exists_right_inverse_linear_map_of_surjective

added theorem linear_independent.inl_union_inr

added theorem linear_independent.ne_zero

added theorem linear_independent.union

deleted theorem linear_independent_inl_union_inr

deleted theorem linear_independent_union

added theorem linear_map.exists_left_inverse_of_injective

added theorem linear_map.exists_right_inverse_of_surjective

deleted theorem ne_zero_of_linear_independent

Modified src/linear_algebra/dual.lean

Modified src/linear_algebra/finite_dimensional.lean