Basic

📁 Source: Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean

Statistics

Metric	Count
Definitions `charmatrix`, `charpoly`	2
Theorems `charmatrix`, `charpoly`, `of_charmatrix`, `aeval_self_charpoly`, `charmatrix_apply`, `charmatrix_apply_eq`, `charmatrix_apply_ne`, `charmatrix_blockTriangular_iff`, `charmatrix_diagonal`, `charmatrix_fromBlocks`, `charmatrix_map`, `charmatrix_natCast`, `charmatrix_ofNat`, `charmatrix_one`, `charmatrix_reindex`, `charmatrix_toSquareBlock`, `charmatrix_transpose`, `charmatrix_zero`, `charpoly_diagonal`, `charpoly_fromBlocks_zero₁₂`, `charpoly_fromBlocks_zero₂₁`, `charpoly_isEmpty`, `charpoly_map`, `charpoly_mul_comm`, `charpoly_mul_comm'`, `charpoly_mul_comm_of_le`, `charpoly_natCast`, `charpoly_ofNat`, `charpoly_of_upperTriangular`, `charpoly_one`, `charpoly_reindex`, `charpoly_sub_scalar`, `charpoly_transpose`, `charpoly_units_conj`, `charpoly_units_conj'`, `charpoly_vecMulVec`, `charpoly_zero`, `eval_charpoly`, `matPolyEquiv_charmatrix`	39
Total	41

Matrix

Definitions

Name	Category	Theorems
`charmatrix` 📖	CompOp	20 math math: `Algebra.Norm.Transitivity.polyToMatrix_cornerAddX`, `charmatrix_reindex`, `charmatrix_toSquareBlock`, `charmatrix_apply_eq`, `charmatrix_apply_ne`, `charmatrix_blockTriangular_iff`, `charmatrix_fromBlocks`, `charmatrix_apply_natDegree`, `matPolyEquiv_charmatrix`, `charmatrix_natCast`, `BlockTriangular.charmatrix`, `charmatrix_one`, `charmatrix_map`, `charmatrix_apply_natDegree_le`, `charmatrix_apply`, `charmatrix_ofNat`, `charmatrix_transpose`, `matPolyEquiv_eq_X_pow_sub_C`, `charmatrix_diagonal`, `charmatrix_zero`
`charpoly` 📖	CompOp	63 math math: `LinearMap.charpoly_def`, `pow_eq_aeval_mod_charpoly`, `coeff_charpoly_mem_ideal_pow`, `ZMod.charpoly_pow_card`, `charpoly_map`, `charpoly_units_conj'`, `mem_spectrum_iff_isRoot_charpoly`, `trace_eq_neg_charpoly_coeff`, `charpoly_natCast`, `IsHermitian.eigenvalues_eq_eigenvalues_iff`, `charpoly_mul_comm_of_le`, `minpoly_dvd_charpoly`, `charpoly_of_upperTriangular`, `charpoly_sub_scalar`, `IsHermitian.charpoly_cfc_eq`, `charpoly_zero`, `charpoly_degree_eq_dim`, `charpoly_leftMulMatrix`, `charpoly.univ_coeff_eval₂Hom`, `charpoly_fromBlocks_zero₂₁`, `charpoly_toLin`, `reverse_charpoly`, `det_eq_prod_roots_charpoly_of_splits`, `charpoly_one`, `trace_eq_sum_roots_charpoly`, `IsHermitian.roots_charpoly_eq_eigenvalues`, `IsHermitian.splits_charpoly`, `LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff`, `IsHermitian.sort_roots_charpoly_eq_eigenvalues₀`, `charpoly_toLin'`, `trace_eq_sum_roots_charpoly_of_splits`, `trace_eq_neg_charpoly_nextCoeff`, `charpoly_fin_two`, `charpoly_units_conj`, `FiniteField.Matrix.charpoly_pow_card`, `charpoly_mulVecLin`, `charpoly_coeff_eq_prod_coeff_of_le`, `charpoly_isEmpty`, `charpoly_natDegree_eq_dim`, `charpoly_fromBlocks_zero₁₂`, `charpoly_sub_diagonal_degree_lt`, `eval_charpoly`, `charpoly_vecMulVec`, `charpoly_mul_comm`, `IsHermitian.roots_charpoly_eq_eigenvalues₀`, `det_eq_prod_roots_charpoly`, `charpoly_inv`, `charpoly.univ_map_eval₂Hom`, `charpoly_transpose`, `charpoly_mul_comm'`, `aeval_self_charpoly`, `charpoly_monic`, `charpoly_reindex`, `IsHermitian.charpoly_eq`, `charpoly_diagonal`, `charpoly_ofNat`, `aeval_eq_aeval_mod_charpoly`, `det_eq_sign_charpoly_coeff`, `BlockTriangular.charpoly`, `charpoly_of_card_eq_two`, `LinearMap.charpoly_toMatrix`, `LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly`, `isNilpotent_charpoly_sub_pow_of_isNilpotent`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_self_charpoly` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix` `Polynomial.semiring` `semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `instAlgebra` `AlgHom.funLike` `Polynomial.aeval` `charpoly` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`adjugate_mul` `Polynomial.eval_map` `matPolyEquiv_smul_one` `Polynomial.eval_mul_X_sub_C` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `matPolyEquiv_charmatrix`
`charmatrix_apply` 📖	mathematical	—	`charmatrix` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instSub` `CommRing.toRing` `diagonal` `Polynomial.instZero` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	—
`charmatrix_apply_eq` 📖	mathematical	—	`charmatrix` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`diagonal_apply_eq`
`charmatrix_apply_ne` 📖	mathematical	—	`charmatrix` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instNeg` `CommRing.toRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`diagonal_apply_ne`
`charmatrix_blockTriangular_iff` 📖	mathematical	—	`BlockTriangular` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `Polynomial.instZero` `charmatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`charmatrix.eq_1` `scalar_apply` `RingHom.mapMatrix_apply` `BlockTriangular.sub_iff_right` `blockTriangular_diagonal`
`charmatrix_diagonal` 📖	mathematical	—	`charmatrix` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instZero` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`charmatrix.eq_1` `scalar_apply` `RingHom.mapMatrix_apply` `diagonal_map` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `diagonal_sub`
`charmatrix_fromBlocks` 📖	mathematical	—	`charmatrix` `instFintypeSum` `fromBlocks` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix` `neg` `Polynomial.instNeg` `CommRing.toRing` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`ext` `Polynomial.ext` `Polynomial.coeff_sub` `zero_sub` `Polynomial.coeff_neg`
`charmatrix_map` 📖	mathematical	—	`charmatrix` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Polynomial` `Polynomial.map`	—	`ext` `Polynomial.ext` `map_map` `Polynomial.coeff_sub` `Polynomial.map_sub` `Polynomial.map_X` `Polynomial.map_C` `zero_sub` `Polynomial.coeff_neg` `Polynomial.map_neg`
`charmatrix_natCast` 📖	mathematical	—	`charmatrix` `Matrix` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `diagonal` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instZero` `Polynomial.instSub` `Polynomial.X` `Polynomial.instNatCast`	—	`charmatrix_diagonal`
`charmatrix_ofNat` 📖	mathematical	—	`charmatrix` `diagonal` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instZero` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X`	—	`charmatrix_natCast`
`charmatrix_one` 📖	mathematical	—	`charmatrix` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `diagonal` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instZero` `Polynomial.instSub` `Polynomial.X` `Polynomial.instOne`	—	`charmatrix_diagonal`
`charmatrix_reindex` 📖	mathematical	—	`charmatrix` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`ext` `Polynomial.ext` `charmatrix.congr_simp` `charmatrix_apply_eq` `Polynomial.coeff_sub` `charmatrix_apply_ne` `Polynomial.coeff_neg` `EquivLike.toEmbeddingLike`
`charmatrix_toSquareBlock` 📖	mathematical	—	`charmatrix` `Subtype.fintype` `toSquareBlock` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`ext`
`charmatrix_transpose` 📖	mathematical	—	`charmatrix` `transpose` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`transpose_sub` `diagonal_transpose`
`charmatrix_zero` 📖	mathematical	—	`charmatrix` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `nonAssocSemiring` `RingHom.instFunLike` `scalar` `Polynomial.X`	—	`map_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `sub_zero`
`charpoly_diagonal` 📖	mathematical	—	`charpoly` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.prod` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRing.toCommMonoid` `Polynomial.commRing` `Finset.univ` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`det.congr_simp` `charmatrix_diagonal` `det_diagonal`
`charpoly_fromBlocks_zero₁₂` 📖	mathematical	—	`charpoly` `instFintypeSum` `fromBlocks` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instMul`	—	`det.congr_simp` `charmatrix_fromBlocks` `map_zero` `Polynomial.C_0` `neg_zero` `det_fromBlocks_zero₁₂`
`charpoly_fromBlocks_zero₂₁` 📖	mathematical	—	`charpoly` `instFintypeSum` `fromBlocks` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instMul`	—	`det.congr_simp` `charmatrix_fromBlocks` `map_zero` `Polynomial.C_0` `neg_zero` `det_fromBlocks_zero₂₁`
`charpoly_isEmpty` 📖	mathematical	—	`charpoly` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instOne`	—	`coe_det_isEmpty`
`charpoly_map` 📖	mathematical	—	`charpoly` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Polynomial.map`	—	`charpoly.eq_1` `charmatrix_map` `Polynomial.coe_mapRingHom` `RingHom.map_det` `RingHom.mapMatrix_apply`
`charpoly_mul_comm` 📖	mathematical	—	`charpoly` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`IsRegular.left` `Polynomial.isRegular_X_pow` `charpoly_mul_comm'`
`charpoly_mul_comm'` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instMul` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Fintype.card` `charpoly` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`fromBlocks_multiply` `mul_neg` `mul_one` `mul_zero` `mul_neg` `zero_add` `mul_one` `one_mul` `neg_add_cancel` `one_mul` `map_mul` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `neg_smul` `smul_eq_mul_diagonal` `neg_mul` `zero_mul` `add_zero` `neg_mul` `scalar_comm` `add_neg_cancel` `sub_eq_add_neg` `det_fromBlocks_zero₂₁` `neg_add_eq_sub` `neg_sub` `det_neg` `det.congr_simp` `diagonal_neg` `det_diagonal` `Finset.prod_const` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.one_pow` `IsRegular.left` `IsUnit.isRegular` `IsUnit.pow` `isUnit_neg_one` `det_mul_comm`
`charpoly_mul_comm_of_le` 📖	mathematical	`Fintype.card`	`charpoly` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instMul` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Fintype.card`	—	`IsRegular.left` `Polynomial.isRegular_X_pow` `mul_assoc` `pow_add` `charpoly_mul_comm'`
`charpoly_natCast` 📖	mathematical	—	`charpoly` `Matrix` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `Polynomial.X` `Polynomial.instNatCast` `Fintype.card`	—	`det.congr_simp` `charmatrix_natCast` `det_diagonal` `Finset.prod_const`
`charpoly_ofNat` 📖	mathematical	—	`charpoly` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `Fintype.card`	—	`charpoly_natCast`
`charpoly_of_upperTriangular` 📖	mathematical	`BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`charpoly` `Finset.prod` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRing.toCommMonoid` `Polynomial.commRing` `Finset.univ` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`det_of_upperTriangular` `BlockTriangular.charmatrix` `Finset.prod_congr` `charmatrix_apply_eq`
`charpoly_one` 📖	mathematical	—	`charpoly` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `Polynomial.X` `Polynomial.instOne` `Fintype.card`	—	`det.congr_simp` `charmatrix_one` `det_diagonal` `Finset.prod_const`
`charpoly_reindex` 📖	mathematical	—	`charpoly` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex`	—	`charmatrix_reindex` `det_reindex_self`
`charpoly_sub_scalar` 📖	mathematical	—	`charpoly` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `nonAssocSemiring` `RingHom.instFunLike` `scalar` `Polynomial.comp` `Polynomial` `Polynomial.instAdd` `Polynomial.X` `Polynomial.semiring` `Polynomial.C`	—	`det_apply` `Polynomial.sum_comp` `Finset.sum_congr` `Polynomial.smul_comp` `Units.instIsScalarTower` `IsScalarTower.right` `Polynomial.prod_comp` `Finset.prod_congr` `charmatrix.congr_simp` `charmatrix_apply_eq` `diagonal_apply_eq` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Polynomial.sub_comp` `Polynomial.X_comp` `Polynomial.C_comp` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `charmatrix_apply_ne` `diagonal_apply_ne` `sub_zero` `Polynomial.neg_comp`
`charpoly_transpose` 📖	mathematical	—	`charpoly` `transpose`	—	`det.congr_simp` `charmatrix_transpose` `det_transpose`
`charpoly_units_conj` 📖	mathematical	—	`charpoly` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units` `Units.instInv`	—	`charpoly_mul_comm` `mul_assoc` `charpoly.congr_simp` `coe_units_inv` `nonsing_inv_mul` `one_mul`
`charpoly_units_conj'` 📖	mathematical	—	`charpoly` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units` `Units.instInv`	—	`charpoly_units_conj`
`charpoly_vecMulVec` 📖	mathematical	—	`charpoly` `vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instSub` `CommRing.toRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Fintype.card` `Algebra.toSMul` `Polynomial.algebraOfAlgebra` `Algebra.id` `dotProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`isEmpty_or_nonempty` `charpoly_isEmpty` `Fintype.card_eq_zero` `pow_zero` `dotProduct_of_isEmpty` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `zero_smul` `sub_zero` `NeZero.one_le` `Fintype.instNeZeroNatCardOfNonempty` `vecMulVec_eq` `charpoly_mul_comm_of_le` `charpoly.eq_1` `charmatrix.eq_1` `Fintype.card_unique` `det_unique` `diagonal_apply_eq` `dotProduct_comm` `mul_sub` `Polynomial.X_pow_mul_C` `Polynomial.smul_eq_C_mul`
`charpoly_zero` 📖	mathematical	—	`charpoly` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Fintype.card`	—	`det.congr_simp` `charmatrix_zero` `det_diagonal` `Finset.prod_const`
`eval_charpoly` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly` `det` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `nonAssocSemiring` `RingHom.instFunLike` `scalar`	—	`charpoly.eq_1` `Polynomial.coe_evalRingHom` `RingHom.map_det` `charmatrix.eq_1` `ext` `eq_or_ne` `diagonal_apply_eq` `Polynomial.eval_sub` `Polynomial.eval_X` `Polynomial.eval_C` `diagonal_apply_ne` `zero_sub` `Polynomial.eval_neg`
`matPolyEquiv_charmatrix` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `Polynomial.semiring` `instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv` `charmatrix` `Polynomial.instSub` `instRing` `CommRing.toRing` `Polynomial.X` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`Polynomial.ext` `ext` `matPolyEquiv_coeff_apply` `Polynomial.coeff_sub` `charmatrix_apply_eq` `Polynomial.coeff_X` `Polynomial.coeff_C` `one_apply_eq` `sub_zero` `zero_sub` `sub_self` `charmatrix_apply_ne` `Polynomial.coeff_neg` `one_apply_ne` `neg_zero`

Matrix.BlockTriangular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charmatrix` 📖	mathematical	`Matrix.BlockTriangular` `Preorder.toLT` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Matrix.BlockTriangular` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `Polynomial.instZero` `Matrix.charmatrix`	—	`Matrix.charmatrix_blockTriangular_iff`
`charpoly` 📖	mathematical	`Matrix.BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Matrix.charpoly` `Finset.prod` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRing.toCommMonoid` `Polynomial.commRing` `Finset.image` `LinearOrder.toDecidableEq` `Finset.univ` `Subtype.fintype` `Matrix.toSquareBlock`	—	`det` `charmatrix` `Finset.prod_congr` `Matrix.det.congr_simp` `Matrix.charmatrix_toSquareBlock`
`of_charmatrix` 📖	mathematical	`Matrix.BlockTriangular` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `Polynomial.instZero` `Matrix.charmatrix`	`Matrix.BlockTriangular` `Preorder.toLT` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Matrix.charmatrix_blockTriangular_iff`

---

← Back to Index