Commit 2023-04-21 04:27 79366def

View on Github →

feat: port LinearAlgebra.Matrix.Adjugate (#3554)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Adjugate.lean

added theorem AlgHom.map_adjugate

added def Matrix.adjugate

added theorem Matrix.adjugate_adjugate'

added theorem Matrix.adjugate_adjugate

added theorem Matrix.adjugate_apply

added theorem Matrix.adjugate_conjTranspose

added theorem Matrix.adjugate_def

added theorem Matrix.adjugate_diagonal

added theorem Matrix.adjugate_eq_one_of_card_eq_one

added theorem Matrix.adjugate_fin_one

added theorem Matrix.adjugate_fin_two

added theorem Matrix.adjugate_fin_two_of

added theorem Matrix.adjugate_fin_zero

added theorem Matrix.adjugate_mul

added theorem Matrix.adjugate_mul_distrib

added theorem Matrix.adjugate_mul_distrib_aux

added theorem Matrix.adjugate_one

added theorem Matrix.adjugate_pow

added theorem Matrix.adjugate_reindex

added theorem Matrix.adjugate_smul

added theorem Matrix.adjugate_submatrix_equiv_self

added theorem Matrix.adjugate_subsingleton

added theorem Matrix.adjugate_transpose

added theorem Matrix.adjugate_zero

added def Matrix.cramer

added def Matrix.cramerMap

added theorem Matrix.cramerMap_is_linear

added theorem Matrix.cramer_apply

added theorem Matrix.cramer_eq_adjugate_mulVec

added theorem Matrix.cramer_is_linear

added theorem Matrix.cramer_one

added theorem Matrix.cramer_reindex

added theorem Matrix.cramer_row_self

added theorem Matrix.cramer_smul

added theorem Matrix.cramer_submatrix_equiv

added theorem Matrix.cramer_subsingleton_apply

added theorem Matrix.cramer_transpose_apply

added theorem Matrix.cramer_transpose_row_self

added theorem Matrix.cramer_zero

added theorem Matrix.det_adjugate

added theorem Matrix.det_smul_adjugate_adjugate

added theorem Matrix.isRegular_of_isLeftRegular_det

added theorem Matrix.mulVec_cramer

added theorem Matrix.mul_adjugate

added theorem Matrix.mul_adjugate_apply

added theorem Matrix.sum_cramer

added theorem Matrix.sum_cramer_apply

added theorem RingHom.map_adjugate