Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 14:26 ecd5234f

View on Github →

feat(linear_algebra): basis on R × R, and relation between matrices and linear maps in this basis (#15119)

Estimated changes

Modified src/algebra/big_operators/fin.lean

modified theorem fin.prod_univ_two

Modified src/linear_algebra/basis.lean

added theorem basis.coe_fin_two_prod_repr

added theorem basis.fin_two_prod_one

added theorem basis.fin_two_prod_zero

Modified src/linear_algebra/determinant.lean

added theorem linear_map.det_to_lin

Modified src/linear_algebra/matrix/determinant.lean

added theorem matrix.det_fin_one_mk

added theorem matrix.det_fin_two_mk

Modified src/linear_algebra/matrix/to_lin.lean

added theorem matrix.to_lin_fin_two_prod

added theorem matrix.to_lin_fin_two_prod_apply

Modified src/topology/algebra/module/finite_dimension.lean

added theorem linear_map.det_to_continuous_linear_map

added theorem matrix.to_lin_fin_two_prod_to_continuous_linear_map