Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-11 14:09 01c3b8f3

View on Github →

feature(algebra/linear_algebra): define linear equivalence

Estimated changes

Modified algebra/linear_algebra/basic.lean

added def equiv_of_is_basis

added theorem linear_equiv.linear_inv

added def linear_equiv.refl

added def linear_equiv.symm

added def linear_equiv.trans

added structure linear_equiv

added theorem linear_independent_singleton

added theorem mem_span_insert

added theorem set.diff_self