Coeff

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

Statistics

Metric	Count
Definitions `charpolyRev`	1
Theorems `aeval_eq_aeval_mod_charpoly`, `charmatrix_apply_natDegree`, `charmatrix_apply_natDegree_le`, `charpoly_coeff_eq_prod_coeff_of_le`, `charpoly_degree_eq_dim`, `charpoly_fin_two`, `charpoly_inv`, `charpoly_monic`, `charpoly_natDegree_eq_dim`, `charpoly_of_card_eq_two`, `charpoly_sub_diagonal_degree_lt`, `coeff_charpolyRev_eq_neg_trace`, `coeff_charpoly_mem_ideal_pow`, `coeff_det_one_add_X_smul_one`, `derivative_det_one_add_X_smul`, `derivative_det_one_add_X_smul_aux`, `det_eq_sign_charpoly_coeff`, `det_one_add_X_smul`, `det_one_add_smul`, `eval_charpolyRev`, `isNilpotent_charpoly_sub_pow_of_isNilpotent`, `isNilpotent_trace_of_isNilpotent`, `isUnit_charpolyRev_of_isNilpotent`, `pow_eq_aeval_mod_charpoly`, `reverse_charpoly`, `trace_eq_neg_charpoly_coeff`, `trace_eq_neg_charpoly_nextCoeff`, `matPolyEquiv_eq_X_pow_sub_C`	28
Total	29

Matrix

Definitions

Name	Category	Theorems
`charpolyRev` 📖	CompOp	5 math math: `reverse_charpoly`, `eval_charpolyRev`, `coeff_charpolyRev_eq_neg_trace`, `isUnit_charpolyRev_of_isNilpotent`, `charpoly_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_eq_aeval_mod_charpoly` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix` `Polynomial.semiring` `semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `instAlgebra` `AlgHom.funLike` `Polynomial.aeval` `Polynomial.modByMonic` `CommRing.toRing` `charpoly`	—	`Polynomial.aeval_modByMonic_eq_self_of_root` `charpoly_monic` `aeval_self_charpoly`
`charmatrix_apply_natDegree` 📖	mathematical	—	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charmatrix`	—	`charmatrix.congr_simp` `charmatrix_apply_eq` `Polynomial.natDegree_sub_C` `Polynomial.natDegree_X` `charmatrix_apply_ne` `Polynomial.natDegree_neg` `Polynomial.natDegree_C`
`charmatrix_apply_natDegree_le` 📖	mathematical	—	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charmatrix`	—	`charmatrix.congr_simp` `charmatrix_apply_eq` `Polynomial.natDegree_sub_C` `charmatrix_apply_ne` `Polynomial.natDegree_neg` `Polynomial.natDegree_C`
`charpoly_coeff_eq_prod_coeff_of_le` 📖	mathematical	`Fintype.card`	`Polynomial.coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly` `Finset.prod` `Polynomial` `CommRing.toCommMonoid` `Polynomial.commRing` `Finset.univ` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`eq_of_sub_eq_zero` `Polynomial.coeff_sub` `Polynomial.coeff_eq_zero_of_degree_lt` `lt_of_lt_of_le` `charpoly_sub_diagonal_degree_lt` `Nat.cast_le` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero`
`charpoly_degree_eq_dim` 📖	mathematical	—	`Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Fintype.card`	—	`det_eq_one_of_card_eq_zero` `Polynomial.degree_one` `CharP.cast_eq_zero` `CharP.ofCharZero` `WithBot.charZero` `Nat.instCharZero` `sub_add_cancel` `Polynomial.degree_eq_iff_natDegree_eq_of_pos` `Polynomial.natDegree_prod'` `Finset.prod_congr` `Polynomial.Monic.leadingCoeff` `Polynomial.monic_X_sub_C` `Finset.prod_const_one` `NeZero.one` `Finset.sum_congr` `Polynomial.natDegree_X_sub_C` `Finset.card_univ` `Finset.sum_const` `smul_eq_mul` `mul_one` `Polynomial.degree_add_eq_right_of_degree_lt` `lt_trans` `charpoly_sub_diagonal_degree_lt` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass`
`charpoly_fin_two` 📖	mathematical	—	`charpoly` `Fin.fintype` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instAdd` `Polynomial.instSub` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `det`	—	`charpoly_of_card_eq_two` `Fintype.card_fin`
`charpoly_inv` 📖	mathematical	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`charpoly` `inv` `Polynomial` `Polynomial.instMul` `Monoid.toNatPow` `Polynomial.semiring` `Polynomial.instNeg` `CommRing.toRing` `Polynomial.instOne` `Fintype.card` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Ring.inverse` `det` `charpolyRev`	—	`det.congr_simp` `inv_mul_of_invertible` `det_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul` `det_mul` `det_nonsing_inv` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative` `RingHom.map_det` `mul_sub` `mul_inv_of_invertible` `map_one` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `neg_sub` `det_neg` `det_one_sub_mul_comm` `smul_eq_diagonal_mul`
`charpoly_monic` 📖	mathematical	—	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `charpoly.eq_1` `det_eq_one_of_card_eq_zero` `Polynomial.monic_one` `Polynomial.monic_prod_of_monic` `Polynomial.Monic.eq_1` `Polynomial.leadingCoeff_add_of_degree_lt` `charpoly_degree_eq_dim` `neg_sub` `Polynomial.degree_neg` `lt_trans` `charpoly_sub_diagonal_degree_lt` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `sub_add_cancel`
`charpoly_natDegree_eq_dim` 📖	mathematical	—	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly` `Fintype.card`	—	`Polynomial.natDegree_eq_of_degree_eq_some` `charpoly_degree_eq_dim`
`charpoly_of_card_eq_two` 📖	mathematical	`Fintype.card`	`charpoly` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instAdd` `Polynomial.instSub` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `det`	—	`Fintype.card_pos_iff` `Polynomial.ext` `det_eq_sign_charpoly_coeff` `Even.neg_pow` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `one_mul` `Polynomial.coeff_add` `Polynomial.coeff_sub` `Polynomial.coeff_X_pow` `Nat.instCharZero` `Polynomial.mul_coeff_zero` `Polynomial.coeff_C_zero` `Polynomial.coeff_X_zero` `MulZeroClass.mul_zero` `sub_self` `zero_add` `trace_eq_neg_charpoly_coeff` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `neg_mul` `sub_neg_eq_add` `Polynomial.coeff_mul_X` `Polynomial.coeff_C_succ` `add_zero` `sub_zero` `charpoly_natDegree_eq_dim` `Polynomial.Monic.leadingCoeff` `charpoly_monic` `Polynomial.coeff_eq_zero_of_natDegree_lt` `not_lt` `Finset.mem_range` `Polynomial.coeff_C_mul` `Polynomial.coeff_X` `Polynomial.coeff_C`
`charpoly_sub_diagonal_degree_lt` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial` `Polynomial.instSub` `CommRing.toRing` `charpoly` `Finset.prod` `CommRing.toCommMonoid` `Polynomial.commRing` `Finset.univ` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Fintype.card`	—	`charpoly.eq_1` `det_apply'` `Finset.insert_erase` `Finset.mem_univ` `Finset.sum_insert` `Finset.notMem_erase` `add_comm` `Equiv.Perm.sign_refl` `Int.cast_one` `Finset.prod_congr` `charmatrix_apply_eq` `one_mul` `add_sub_cancel_right` `Polynomial.mem_degreeLT` `Submodule.sum_mem` `Polynomial.C_eq_intCast` `Polynomial.C_mul'` `Submodule.smul_mem` `lt_of_le_of_lt` `Polynomial.degree_le_natDegree` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `le_trans` `Polynomial.natDegree_prod_le` `Finset.card_eq_sum_ones` `Finset.sum_filter` `Finset.sum_le_sum` `charmatrix_apply_natDegree_le` `Equiv.Perm.fixed_point_card_lt_of_ne_one` `Finset.ne_of_mem_erase`
`coeff_charpolyRev_eq_neg_trace` 📖	mathematical	—	`Polynomial.coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpolyRev` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `isEmpty_or_nonempty` `coe_det_isEmpty` `Polynomial.coeff_one` `trace_eq_zero_of_isEmpty` `neg_zero` `reverse_charpoly` `Polynomial.coeff_one_reverse` `charpoly_natDegree_eq_dim` `trace_eq_neg_charpoly_coeff` `neg_neg`
`coeff_charpoly_mem_ideal_pow` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Fintype.card` `Polynomial.coeff` `charpoly`	—	`IsScalarTower.right` `det_apply` `Polynomial.finset_sum_coeff` `sum_mem` `Submodule.addSubmonoidClass` `Polynomial.coeff_smul` `Submodule.smul_mem_iff'` `Units.instIsScalarTower` `Finset.sum_const` `Finset.card_univ` `smul_eq_mul` `mul_one` `Polynomial.coeff_prod_mem_ideal_pow_tsub` `tsub_zero` `Nat.instOrderedSub` `pow_one` `charmatrix_apply` `Polynomial.coeff_sub` `smul_one_eq_diagonal` `smul_apply` `Polynomial.coeff_X_mul_zero` `Polynomial.coeff_C_zero` `zero_sub` `neg_mem_iff` `NonUnitalSubringClass.toNegMemClass` `instNonUnitalSubringClassIdeal` `add_comm` `tsub_self_add` `Nat.instCanonicallyOrderedAdd` `pow_zero` `Ideal.one_eq_top` `Submodule.mem_top`
`coeff_det_one_add_X_smul_one` 📖	mathematical	—	`Polynomial.coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `det` `Polynomial` `Polynomial.commRing` `Matrix` `add` `Polynomial.instAdd` `one` `Polynomial.instZero` `Polynomial.instOne` `smul` `Algebra.toSMul` `Polynomial.commSemiring` `Algebra.id` `Polynomial.X` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Polynomial.coeff_derivative` `zero_add` `Nat.cast_zero` `mul_one`
`derivative_det_one_add_X_smul` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `det` `Polynomial.commRing` `Matrix` `add` `Polynomial.instAdd` `one` `Polynomial.instZero` `Polynomial.instOne` `smul` `Algebra.toSMul` `Polynomial.commSemiring` `Algebra.id` `Polynomial.X` `map` `RingHom` `RingHom.instFunLike` `Polynomial.C` `trace`	—	`RingHomInvPair.ids` `det_reindexLinearEquiv_self` `ext` `Polynomial.ext` `map_add` `SemilinearMapClass.toAddHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `submatrix_one_equiv` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Polynomial.X_mul_C` `Polynomial.coeff_add` `Polynomial.coeff_C_mul` `Equiv.sum_comp` `Finset.sum_congr` `derivative_det_one_add_X_smul_aux`
`derivative_det_one_add_X_smul_aux` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `det` `Fin.fintype` `Polynomial.commRing` `Matrix` `add` `Polynomial.instAdd` `one` `Polynomial.instZero` `Polynomial.instOne` `smul` `Algebra.toSMul` `Polynomial.commSemiring` `Algebra.id` `Polynomial.X` `map` `RingHom` `RingHom.instFunLike` `Polynomial.C` `trace`	—	`det_fin_zero` `Polynomial.derivative_one` `Polynomial.eval_zero` `trace_eq_zero_of_isEmpty` `Fin.isEmpty'` `det_succ_row_zero` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Polynomial.eval_finset_sum` `Finset.sum_congr` `Polynomial.X_mul_C` `Polynomial.derivative_mul` `map_add` `SemilinearMapClass.toAddHomClass` `Polynomial.derivative_C` `MulZeroClass.zero_mul` `Polynomial.derivative_X` `mul_one` `zero_add` `Polynomial.eval_add` `Polynomial.eval_mul` `Polynomial.eval_C` `Polynomial.eval_X` `MulZeroClass.mul_zero` `add_zero` `Polynomial.eval_pow` `Polynomial.eval_neg` `Polynomial.eval_one` `eval_det_add_X_smul` `Finset.sum_eq_single` `one_apply_ne'` `det_eq_zero_of_column_eq_zero` `submatrix_apply` `Fin.succAbove_of_castSucc_lt` `lt_of_le_of_ne` `one_apply_ne` `instLawfulBCmpCompare_mathlib` `Finset.mem_univ` `pow_zero` `one_apply_eq` `one_mul` `det.congr_simp` `submatrix_one` `Fin.succ_injective` `det_one` `trace_submatrix_succ`
`det_eq_sign_charpoly_coeff` 📖	mathematical	—	`det` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Fintype.card` `Polynomial.coeff` `charpoly`	—	`Polynomial.coeff_zero_eq_eval_zero` `charpoly.eq_1` `eval_det` `matPolyEquiv_charmatrix` `det_smul` `det.congr_simp` `diagonal_zero` `Polynomial.eval_sub` `Polynomial.eval_X` `Polynomial.eval_C` `zero_sub` `smul_neg` `neg_smul` `one_smul` `neg_neg`
`det_one_add_X_smul` 📖	mathematical	—	`det` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.commRing` `Matrix` `add` `Polynomial.instAdd` `one` `Polynomial.instZero` `Polynomial.instOne` `smul` `Algebra.toSMul` `Polynomial.commSemiring` `Algebra.id` `Polynomial.X` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.algebraOfAlgebra` `trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.instMul` `Polynomial.divX` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Algebra.smul_def` `Polynomial.C_eq_algebraMap` `pow_two` `mul_assoc` `add_assoc` `add_mul` `Distrib.rightDistribClass` `coeff_det_one_add_X_smul_one` `Polynomial.coeff_divX` `add_comm` `Polynomial.divX_mul_X_add` `RingHom.map_one` `Polynomial.coeff_zero_eq_eval_zero` `eval_det_add_X_smul` `det_one` `Polynomial.eval_one`
`det_one_add_smul` 📖	mathematical	—	`det` `Matrix` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Distrib.toMul` `trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Polynomial.eval` `Polynomial.divX` `Polynomial` `Polynomial.commRing` `Polynomial.instAdd` `Polynomial.instZero` `Polynomial.instOne` `Polynomial.commSemiring` `Polynomial.X` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`eval_det` `det.congr_simp` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `matPolyEquiv_map_smul` `Polynomial.map_X` `matPolyEquiv_map_C` `Polynomial.X_mul_C` `Polynomial.eval_add` `Polynomial.eval_one` `Polynomial.eval_mul_X` `Polynomial.eval_C` `Polynomial.eval_smul` `IsScalarTower.right` `Polynomial.eval_X` `Polynomial.eval_mul` `Polynomial.eval_pow` `det_one_add_X_smul`
`eval_charpolyRev` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `charpolyRev` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`charpolyRev.eq_1` `Polynomial.coe_evalRingHom` `RingHom.map_det` `det_one` `ext` `eq_or_ne` `one_apply_eq` `Polynomial.X_mul_C` `Polynomial.eval_sub` `Polynomial.eval_one` `Polynomial.eval_mul` `Polynomial.eval_C` `Polynomial.eval_X` `MulZeroClass.mul_zero` `sub_zero` `one_apply_ne` `zero_sub` `Polynomial.eval_neg` `neg_zero`
`isNilpotent_charpoly_sub_pow_of_isNilpotent` 📖	mathematical	`IsNilpotent` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Polynomial` `Polynomial.instZero` `Polynomial.semiring` `Polynomial.instSub` `CommRing.toRing` `charpoly` `Polynomial.X` `Fintype.card`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `Polynomial.modByMonic_add_div` `Polynomial.monic_X` `Polynomial.modByMonic_X` `eval_charpolyRev` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `add_sub_cancel_left` `Polynomial.isUnit_iff'` `isUnit_charpolyRev_of_isNilpotent` `le_trans` `Polynomial.natDegree_sub_le` `charpoly_natDegree_eq_dim` `Polynomial.natDegree_X_pow` `max_self` `Polynomial.isNilpotent_reflect_iff` `Polynomial.reflect_sub` `Polynomial.reverse.eq_1` `reverse_charpoly` `Polynomial.reflect_monomial` `Polynomial.revAt_le` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero`
`isNilpotent_trace_of_isNilpotent` 📖	mathematical	`IsNilpotent` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`isEmpty_or_nonempty` `trace_eq_zero_of_isEmpty` `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent` `isUnit_charpolyRev_of_isNilpotent` `one_ne_zero` `coeff_charpolyRev_eq_neg_trace`
`isUnit_charpolyRev_of_isNilpotent` 📖	mathematical	`IsNilpotent` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`IsUnit` `Polynomial` `Polynomial.semiring` `charpolyRev`	—	`RingHom.mapMatrix_apply` `smul_pow` `IsScalarTower.right` `Algebra.to_smulCommClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `smul_zero` `sub_zero` `one_sub_dvd_one_sub_pow` `isUnit_of_dvd_one` `det_one` `map_dvd` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`pow_eq_aeval_mod_charpoly` 📖	mathematical	—	`Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `instAlgebra` `AlgHom.funLike` `Polynomial.aeval` `Polynomial.modByMonic` `CommRing.toRing` `Ring.toSemiring` `Polynomial.X` `charpoly`	—	`aeval_eq_aeval_mod_charpoly` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X`
`reverse_charpoly` 📖	mathematical	—	`Polynomial.reverse` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly` `charpolyRev`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `LaurentPolynomial.T_add` `neg_add_cancel` `LaurentPolynomial.T_zero` `AlgHom.map_det` `det.congr_simp` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `diagonal_map` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Polynomial.toLaurent_X` `map_map` `Polynomial.toLaurent_comp_C` `smul_eq_diagonal_mul` `map_one` `Polynomial.toLaurent_one` `map_mul` `RingHomClass.toNonUnitalRingHomClass` `det_smul` `smul_sub` `scalar_apply` `diagonal_smul` `Pi.smul_def` `smul_eq_mul` `diagonal_one` `AlgEquiv.map_det` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AlgHomClass.toRingHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `LaurentPolynomial.invert_T` `LaurentPolynomial.invert_comp_C` `Polynomial.toLaurent_injective` `LaurentPolynomial.toLaurent_reverse` `Polynomial.coe_toLaurentAlg` `Function.Involutive.injective` `LaurentPolynomial.involutive_invert` `charpoly_natDegree_eq_dim` `mul_one` `LaurentPolynomial.T_pow` `map_pow` `mul_comm`
`trace_eq_neg_charpoly_coeff` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Polynomial.coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly` `Fintype.card`	—	`charpoly_coeff_eq_prod_coeff_of_le` `le_rfl` `Fintype.card.eq_1` `Polynomial.prod_X_sub_C_coeff_card_pred` `Fintype.card_pos` `neg_neg` `trace.eq_1` `Finset.sum_congr`
`trace_eq_neg_charpoly_nextCoeff` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Polynomial.nextCoeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly`	—	`isEmpty_or_nonempty` `trace_eq_zero_of_isEmpty` `charpoly_isEmpty` `Polynomial.natDegree_one` `neg_zero` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `trace_eq_neg_charpoly_coeff` `charpoly_natDegree_eq_dim`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`matPolyEquiv_eq_X_pow_sub_C` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.semiring` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv` `RingHom` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.mapMatrix` `RingHomClass.toRingHom` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.expand` `Matrix.charmatrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.instSub` `Matrix.instRing` `CommRing.toRing` `Polynomial.X` `Polynomial.C`	—	`Polynomial.ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Matrix.ext` `Polynomial.coeff_sub` `Polynomial.coeff_C` `matPolyEquiv_coeff_apply` `RingHom.mapMatrix_apply` `Matrix.map_apply` `AlgHom.coe_toRingHom` `DMatrix.sub_apply` `Polynomial.coeff_X_pow` `Matrix.charmatrix_apply_eq` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Polynomial.expand_C` `Polynomial.expand_X` `Matrix.one_apply_eq` `sub_zero` `zero_sub` `sub_self` `Matrix.charmatrix_apply_ne` `map_neg` `Polynomial.coeff_neg` `pow_zero` `Matrix.one_apply_ne` `neg_zero`

---

← Back to Index