Commit 2023-05-02 10:05 cc8f26f5

View on Github →

feat: port LinearAlgebra.Determinant (#3694)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Determinant.lean

added theorem AlternatingMap.eq_smul_basis_det

added theorem AlternatingMap.map_basis_eq_zero_iff

added theorem AlternatingMap.map_basis_ne_zero_iff

added theorem Basis.det_apply

added theorem Basis.det_comp

added theorem Basis.det_comp_basis

added theorem Basis.det_isEmpty

added theorem Basis.det_isUnitSMul

added theorem Basis.det_map'

added theorem Basis.det_map

added theorem Basis.det_ne_zero

added theorem Basis.det_reindex

added theorem Basis.det_reindex_symm

added theorem Basis.det_self

added theorem Basis.det_smul_mk_coord_eq_det_update

added theorem Basis.det_unitsSMul

added theorem Basis.det_unitsSMul_self

added theorem Basis.isUnit_det

added theorem LinearEquiv.coe_det

added theorem LinearEquiv.coe_inv_det

added theorem LinearEquiv.coe_ofIsUnitDet

added theorem LinearEquiv.det_coe_symm

added theorem LinearEquiv.det_conj

added theorem LinearEquiv.det_mul_det_symm

added theorem LinearEquiv.det_refl

added theorem LinearEquiv.det_symm

added theorem LinearEquiv.det_symm_mul_det

added theorem LinearEquiv.det_trans

added theorem LinearEquiv.isUnit_det'

added theorem LinearEquiv.isUnit_det

added def LinearEquiv.ofIsUnitDet

added theorem LinearMap.associated_det_comp_equiv

added theorem LinearMap.associated_det_of_eq_comp

added theorem LinearMap.bot_lt_ker_of_det_eq_zero

added theorem LinearMap.coe_det

added theorem LinearMap.detAux_comp

added theorem LinearMap.detAux_def''

added theorem LinearMap.detAux_def'

added theorem LinearMap.detAux_id

added theorem LinearMap.det_cases

added theorem LinearMap.det_comp

added theorem LinearMap.det_conj

added theorem LinearMap.det_eq_det_toMatrix_of_finset

added theorem LinearMap.det_eq_one_of_finrank_eq_zero

added theorem LinearMap.det_eq_one_of_subsingleton

added theorem LinearMap.det_id

added theorem LinearMap.det_smul

added theorem LinearMap.det_toLin'

added theorem LinearMap.det_toLin

added theorem LinearMap.det_toMatrix'

added theorem LinearMap.det_toMatrix

added theorem LinearMap.det_toMatrix_eq_det_toMatrix

added theorem LinearMap.det_zero'

added theorem LinearMap.det_zero

added def LinearMap.equivOfDetNeZero

added theorem LinearMap.finiteDimensional_of_det_ne_one

added theorem LinearMap.isUnit_det

added theorem LinearMap.range_lt_top_of_det_eq_zero

added theorem Matrix.det_comm'

added theorem Matrix.det_comm

added theorem Matrix.det_conj_of_mul_eq_one

added def Matrix.indexEquivOfInv

added theorem Pi.basisFun_det

added def equivOfPiLEquivPi

added theorem is_basis_iff_det