Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-10 13:08 56ff42bd

View on Github →

feat(linear_algebra/matrix/transvection): matrices are generated by transvections and diagonal matrices (#8898) One version of Gauss' pivot: any matrix can be obtained starting from a diagonal matrix and doing elementary moves on rows and columns. Phrased in terms of multiplication by transvections.

Estimated changes

Modified src/algebra/lie/classical.lean

deleted def lie_algebra.special_linear.E

deleted theorem lie_algebra.special_linear.E_apply_one

deleted theorem lie_algebra.special_linear.E_apply_zero

deleted theorem lie_algebra.special_linear.E_diag_zero

deleted theorem lie_algebra.special_linear.E_trace_zero

modified theorem lie_algebra.special_linear.Eb_val

Modified src/data/matrix/basis.lean

added theorem matrix.std_basis_matrix.apply_of_col_ne

added theorem matrix.std_basis_matrix.apply_of_ne

added theorem matrix.std_basis_matrix.apply_of_row_ne

added theorem matrix.std_basis_matrix.apply_same

added theorem matrix.std_basis_matrix.diag_zero

added theorem matrix.std_basis_matrix.mul_left_apply_of_ne

added theorem matrix.std_basis_matrix.mul_left_apply_same

added theorem matrix.std_basis_matrix.mul_of_ne

added theorem matrix.std_basis_matrix.mul_right_apply_of_ne

added theorem matrix.std_basis_matrix.mul_right_apply_same

added theorem matrix.std_basis_matrix.mul_same

added theorem matrix.std_basis_matrix.trace_zero

Modified src/data/matrix/block.lean

added def matrix.is_two_block_diagonal

Modified src/data/nat/basic.lean

added def nat.decreasing_induction'

added def nat.le_rec_on'

Modified src/data/option/basic.lean

added theorem option.to_list_none

added theorem option.to_list_some

Created src/linear_algebra/matrix/transvection.lean

added theorem matrix.det_transvection_of_ne

added theorem matrix.diagonal_transvection_induction

added theorem matrix.diagonal_transvection_induction_of_det_ne_zero

added theorem matrix.mul_transvection_apply_of_ne

added theorem matrix.mul_transvection_apply_same

added theorem matrix.pivot.exists_is_two_block_diagonal_list_transvec_mul_mul_list_transvec

added theorem matrix.pivot.exists_is_two_block_diagonal_of_ne_zero

added theorem matrix.pivot.exists_list_transvec_mul_diagonal_mul_list_transvec

added theorem matrix.pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal

added theorem matrix.pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux

added theorem matrix.pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction

added theorem matrix.pivot.is_two_block_diagonal_list_transvec_col_mul_mul_list_transvec_row

added def matrix.pivot.list_transvec_col

added theorem matrix.pivot.list_transvec_col_mul_last_col

added theorem matrix.pivot.list_transvec_col_mul_last_row

added theorem matrix.pivot.list_transvec_col_mul_last_row_drop

added theorem matrix.pivot.list_transvec_col_mul_mul_list_transvec_row_last_col

added theorem matrix.pivot.list_transvec_col_mul_mul_list_transvec_row_last_row

added def matrix.pivot.list_transvec_row

added theorem matrix.pivot.mul_list_transvec_row_last_col

added theorem matrix.pivot.mul_list_transvec_row_last_col_take

added theorem matrix.pivot.mul_list_transvec_row_last_row

added theorem matrix.pivot.reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal

added def matrix.transvection

added theorem matrix.transvection_mul_apply_of_ne

added theorem matrix.transvection_mul_apply_same

added theorem matrix.transvection_mul_transvection_same

added theorem matrix.transvection_struct.det_to_matrix_prod

added theorem matrix.transvection_struct.inv_mul

added theorem matrix.transvection_struct.mul_inv

added theorem matrix.transvection_struct.mul_sum_inl_to_matrix_prod

added theorem matrix.transvection_struct.prod_mul_reverse_inv_prod

added def matrix.transvection_struct.reindex_equiv

added theorem matrix.transvection_struct.reverse_inv_prod_mul_prod

added def matrix.transvection_struct.sum_inl

added theorem matrix.transvection_struct.sum_inl_to_matrix_prod_mul

added def matrix.transvection_struct.to_matrix

added theorem matrix.transvection_struct.to_matrix_mk

added theorem matrix.transvection_struct.to_matrix_reindex_equiv

added theorem matrix.transvection_struct.to_matrix_reindex_equiv_prod

added theorem matrix.transvection_struct.to_matrix_sum_inl

added structure matrix.transvection_struct

added theorem matrix.transvection_zero

added theorem matrix.update_row_eq_transvection

Modified src/ring_theory/matrix_algebra.lean