Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-04 21:18 0dfba50d

View on Github →

feat(algebra/algebra/basic): alg_equiv.of_linear_equiv (#6495)

Estimated changes

Modified src/algebra/algebra/basic.lean

added def alg_equiv.of_linear_equiv

added theorem alg_equiv.of_linear_equiv_apply

added theorem alg_equiv.of_linear_equiv_to_linear_equiv

added theorem alg_equiv.to_linear_equiv_of_linear_equiv