Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-10 20:43 e62a406b

View on Github →

feat(linear_algebra/determinant): determinant of a block triangular matrix (#6050) Add lemmas for determinants of block triangular matrices.

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.subtype_subtype_equiv_subtype_apply

added theorem equiv.subtype_subtype_equiv_subtype_exists_apply

added theorem equiv.subtype_subtype_equiv_subtype_inter_apply

Modified src/data/matrix/basic.lean

added def matrix.to_block

added theorem matrix.to_block_apply

added def matrix.to_square_block'

added def matrix.to_square_block

added theorem matrix.to_square_block_def'

added theorem matrix.to_square_block_def

added def matrix.to_square_block_prop

added theorem matrix.to_square_block_prop_def

Modified src/group_theory/perm/basic.lean

added theorem equiv.perm.default_perm

Modified src/group_theory/perm/sign.lean

added theorem equiv.perm.perm_maps_to_inl_iff_maps_to_inr

added theorem equiv.perm.perm_on_inl_iff_perm_on_inr

Modified src/linear_algebra/determinant.lean

added theorem matrix.det_eq_elem_of_card_eq_one

added theorem matrix.det_unique

added theorem matrix.upper_two_block_triangular_det

Modified src/linear_algebra/matrix.lean

added def matrix.block_triangular_matrix'

added def matrix.block_triangular_matrix

added theorem matrix.det_of_block_triangular_matrix''

added theorem matrix.det_of_block_triangular_matrix'

added theorem matrix.det_of_block_triangular_matrix

added theorem matrix.det_of_lower_triangular

added theorem matrix.det_of_upper_triangular

added theorem matrix.det_to_block

added theorem matrix.det_to_square_block'

added theorem matrix.det_to_square_block

added theorem matrix.equiv_block_det

added theorem matrix.to_square_block_det''

added theorem matrix.two_block_triangular_det

added theorem matrix.upper_two_block_triangular'

added theorem matrix.upper_two_block_triangular