Commit 2023-04-20 10:27 1e61d3d6

View on Github →

feat: port LinearAlgebra.Matrix.Determinant (#3540)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Determinant.lean

added theorem AlgEquiv.map_det

added theorem AlgHom.map_det

added theorem Matrix.coe_detMonoidHom

added theorem Matrix.coe_det_isEmpty

added def Matrix.detMonoidHom

added def Matrix.detRowAlternating

added theorem Matrix.det_apply'

added theorem Matrix.det_apply

added theorem Matrix.det_blockDiagonal

added theorem Matrix.det_conjTranspose

added theorem Matrix.det_diagonal

added theorem Matrix.det_eq_elem_of_card_eq_one

added theorem Matrix.det_eq_elem_of_subsingleton

added theorem Matrix.det_eq_of_eq_det_one_mul

added theorem Matrix.det_eq_of_eq_mul_det_one

added theorem Matrix.det_eq_of_forall_col_eq_smul_add_pred

added theorem Matrix.det_eq_of_forall_row_eq_smul_add_const

added theorem Matrix.det_eq_of_forall_row_eq_smul_add_const_aux

added theorem Matrix.det_eq_of_forall_row_eq_smul_add_pred

added theorem Matrix.det_eq_of_forall_row_eq_smul_add_pred_aux

added theorem Matrix.det_eq_one_of_card_eq_zero

added theorem Matrix.det_eq_zero_of_column_eq_zero

added theorem Matrix.det_eq_zero_of_row_eq_zero

added theorem Matrix.det_fin_one

added theorem Matrix.det_fin_one_of

added theorem Matrix.det_fin_three

added theorem Matrix.det_fin_two

added theorem Matrix.det_fin_two_of

added theorem Matrix.det_fin_zero

added theorem Matrix.det_fromBlocks_zero₁₂

added theorem Matrix.det_fromBlocks_zero₂₁

added theorem Matrix.det_isEmpty

added theorem Matrix.det_mul

added theorem Matrix.det_mul_aux

added theorem Matrix.det_mul_column

added theorem Matrix.det_mul_comm

added theorem Matrix.det_mul_left_comm

added theorem Matrix.det_mul_right_comm

added theorem Matrix.det_mul_row

added theorem Matrix.det_neg

added theorem Matrix.det_neg_eq_smul

added theorem Matrix.det_one

added theorem Matrix.det_permutation

added theorem Matrix.det_permute

added theorem Matrix.det_pow

added theorem Matrix.det_reindex_self

added theorem Matrix.det_smul

added theorem Matrix.det_smul_of_tower

added theorem Matrix.det_submatrix_equiv_self

added theorem Matrix.det_succ_column

added theorem Matrix.det_succ_column_zero

added theorem Matrix.det_succ_row

added theorem Matrix.det_succ_row_zero

added theorem Matrix.det_transpose

added theorem Matrix.det_unique

added theorem Matrix.det_units_conj'

added theorem Matrix.det_units_conj

added theorem Matrix.det_updateColumn_add

added theorem Matrix.det_updateColumn_add_self

added theorem Matrix.det_updateColumn_add_smul_self

added theorem Matrix.det_updateColumn_smul'

added theorem Matrix.det_updateColumn_smul

added theorem Matrix.det_updateRow_add

added theorem Matrix.det_updateRow_add_self

added theorem Matrix.det_updateRow_add_smul_self

added theorem Matrix.det_updateRow_smul'

added theorem Matrix.det_updateRow_smul

added theorem Matrix.det_zero

added theorem Matrix.det_zero_of_column_eq

added theorem Matrix.det_zero_of_row_eq

added theorem RingEquiv.map_det

added theorem RingHom.map_det