Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-02 17:27 62ec2c57

View on Github →

feat(linear_algebra/matrix): add alg_equiv_matrix (#2919)

Estimated changes

Modified src/linear_algebra/basic.lean

added theorem linear_equiv.arrow_congr_apply

added theorem linear_equiv.arrow_congr_comp

added theorem linear_equiv.conj_apply

added theorem linear_equiv.conj_id

Modified src/linear_algebra/matrix.lean

added def alg_equiv_matrix'

added def alg_equiv_matrix

added def linear_equiv.alg_conj