Documentation Verification Report

MatrixPolynomialAlgebra

📁 Source: Mathlib/RingTheory/MatrixPolynomialAlgebra.lean

Statistics

Metric	Count
Definitions `polyToMatrix`, `matPolyEquiv`	2
Theorems `evalRingHom_mapMatrix_comp_compRingEquiv`, `evalRingHom_mapMatrix_comp_polyToMatrix`, `eval_det`, `eval_det_add_X_smul`, `matPolyEquiv_coeff_apply`, `matPolyEquiv_coeff_apply_aux_1`, `matPolyEquiv_coeff_apply_aux_2`, `matPolyEquiv_diagonal_X`, `matPolyEquiv_eval`, `matPolyEquiv_eval_eq_map`, `matPolyEquiv_map_C`, `matPolyEquiv_map_smul`, `matPolyEquiv_smul_one`, `matPolyEquiv_symm_C`, `matPolyEquiv_symm_X`, `matPolyEquiv_symm_apply_coeff`, `matPolyEquiv_symm_map_eval`, `support_subset_support_matPolyEquiv`	18
Total	20

RingHom

Definitions

Name	Category	Theorems
`polyToMatrix` 📖	CompOp	4 math math: `Algebra.Norm.Transitivity.polyToMatrix_cornerAddX`, `evalRingHom_mapMatrix_comp_polyToMatrix`, `Algebra.Norm.Transitivity.eval_zero_comp_det`, `Algebra.Norm.Transitivity.eval_zero_det_det`

(root)

Definitions

Name	Category	Theorems
`matPolyEquiv` 📖	CompOp	17 math math: `matPolyEquiv_map_smul`, `matPolyEquiv_diagonal_X`, `matPolyEquiv_coeff_apply_aux_1`, `matPolyEquiv_symm_apply_coeff`, `Matrix.matPolyEquiv_charmatrix`, `matPolyEquiv_map_C`, `eval_det`, `matPolyEquiv_symm_C`, `matPolyEquiv_eval_eq_map`, `matPolyEquiv_coeff_apply`, `support_subset_support_matPolyEquiv`, `matPolyEquiv_symm_map_eval`, `matPolyEquiv_eval`, `matPolyEquiv_symm_X`, `matPolyEquiv_coeff_apply_aux_2`, `matPolyEquiv_smul_one`, `matPolyEquiv_eq_X_pow_sub_C`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evalRingHom_mapMatrix_comp_compRingEquiv` 📖	mathematical	—	`RingHom.comp` `Matrix` `Polynomial` `CommSemiring.toSemiring` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `instFintypeProd` `RingHom.mapMatrix` `Polynomial.evalRingHom` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHomClass.toRingHom` `RingEquiv` `Matrix.instMulOfFintypeOfAddCommMonoid` `Polynomial.instMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.addCommMonoid` `Matrix.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Matrix.compRingEquiv` `RingEquiv.toRingHom` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`RingHom.ext` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Matrix.ext`
`evalRingHom_mapMatrix_comp_polyToMatrix` 📖	mathematical	—	`RingHom.comp` `Polynomial` `CommSemiring.toSemiring` `Matrix` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Matrix.nonAssocSemiring` `RingHom.mapMatrix` `Polynomial.evalRingHom` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHom.polyToMatrix`	—	`Polynomial.ringHom_ext'` `RingHom.ext` `Matrix.ext` `Polynomial.map_C` `matPolyEquiv_symm_C` `Polynomial.eval_C` `Polynomial.map_X` `matPolyEquiv_symm_X` `Polynomial.eval_X` `Polynomial.eval_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`eval_det` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.det` `Polynomial` `Polynomial.commRing` `Matrix` `Matrix.semiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Matrix.nonAssocSemiring` `RingHom.instFunLike` `Matrix.scalar` `AlgEquiv` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv`	—	`Polynomial.eval.eq_1` `Polynomial.coe_eval₂RingHom` `RingHom.map_det` `Matrix.ext` `matPolyEquiv_eval`
`eval_det_add_X_smul` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Matrix.det` `Polynomial` `Polynomial.commRing` `Matrix` `Matrix.add` `Polynomial.instAdd` `Matrix.smul` `Algebra.toSMul` `Polynomial.commSemiring` `Algebra.id` `Polynomial.X` `Matrix.map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`Matrix.det.congr_simp` `Algebra.smul_def` `eval_det` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `Polynomial.eval_add` `Algebra.algebraMap_eq_smul_one` `matPolyEquiv_smul_one` `Polynomial.map_X` `Polynomial.X_mul` `Polynomial.eval_mul_X` `MulZeroClass.mul_zero` `add_zero`
`matPolyEquiv_coeff_apply` 📖	mathematical	—	`Polynomial.coeff` `Matrix` `Matrix.semiring` `CommSemiring.toSemiring` `DFunLike.coe` `AlgEquiv` `Polynomial` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv`	—	`Matrix.induction_on'` `Finite.of_fintype` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Polynomial.coeff_add` `matPolyEquiv_coeff_apply_aux_2`
`matPolyEquiv_coeff_apply_aux_1` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `Polynomial` `CommSemiring.toSemiring` `Matrix.semiring` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv` `Matrix.single` `Polynomial.instZero` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.monomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`matrixEquivTensor_apply_single` `AlgEquiv.injective` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgEquiv.apply_symm_apply` `Polynomial.eval₂_monomial` `Algebra.TensorProduct.tmul_pow` `one_pow` `Polynomial.smul_X_eq_monomial` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `Matrix.isScalarTower` `IsScalarTower.right` `Polynomial.isScalarTower` `Algebra.to_smulCommClass` `Matrix.ext` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Polynomial.ext` `Polynomial.coeff_X_pow` `one_mul`
`matPolyEquiv_coeff_apply_aux_2` 📖	mathematical	—	`Polynomial.coeff` `Matrix` `Matrix.semiring` `CommSemiring.toSemiring` `DFunLike.coe` `AlgEquiv` `Polynomial` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv` `Matrix.single` `Polynomial.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Polynomial.induction_on'` `Matrix.ext` `Matrix.single_add` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Polynomial.coeff_add` `Matrix.single.congr_simp` `matPolyEquiv_coeff_apply_aux_1` `Polynomial.coeff_monomial` `Matrix.single_zero`
`matPolyEquiv_diagonal_X` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `Polynomial` `CommSemiring.toSemiring` `Matrix.semiring` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv` `Matrix.diagonal` `Polynomial.instZero` `Polynomial.X`	—	`matPolyEquiv_symm_X` `AlgEquiv.apply_symm_apply`
`matPolyEquiv_eval` 📖	mathematical	—	`Polynomial.eval` `Matrix` `Matrix.semiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Matrix.nonAssocSemiring` `RingHom.instFunLike` `Matrix.scalar` `AlgEquiv` `Polynomial` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv`	—	`matPolyEquiv_eval_eq_map` `Matrix.map_apply`
`matPolyEquiv_eval_eq_map` 📖	mathematical	—	`Polynomial.eval` `Matrix` `Matrix.semiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Matrix.nonAssocSemiring` `RingHom.instFunLike` `Matrix.scalar` `AlgEquiv` `Polynomial` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv` `Matrix.map`	—	`AlgEquiv.symm_apply_apply` `matPolyEquiv_symm_map_eval`
`matPolyEquiv_map_C` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `Polynomial` `CommSemiring.toSemiring` `Matrix.semiring` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv` `Matrix.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`matPolyEquiv_symm_C` `AlgEquiv.apply_symm_apply`
`matPolyEquiv_map_smul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `Polynomial` `CommSemiring.toSemiring` `Matrix.semiring` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv` `Matrix.smul` `Algebra.toSMul` `Polynomial.commSemiring` `Polynomial.instMul` `Polynomial.map` `algebraMap`	—	`one_mul` `smul_mul_assoc` `IsScalarTower.right` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `matPolyEquiv_smul_one`
`matPolyEquiv_smul_one` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `Polynomial` `CommSemiring.toSemiring` `Matrix.semiring` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv` `Matrix.smul` `Algebra.toSMul` `Polynomial.commSemiring` `Matrix.one` `Polynomial.instZero` `Polynomial.instOne` `Polynomial.map` `algebraMap`	—	`Polynomial.ext` `Matrix.ext` `matPolyEquiv_coeff_apply` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Polynomial.coeff_map`
`matPolyEquiv_symm_C` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Polynomial` `Matrix` `Matrix.semiring` `CommSemiring.toSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Matrix.instAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `AlgEquiv.symm` `matPolyEquiv` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Matrix.map`	—	`Polynomial.eval₂_C` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `one_smul`
`matPolyEquiv_symm_X` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Polynomial` `Matrix` `Matrix.semiring` `CommSemiring.toSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Matrix.instAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `AlgEquiv.symm` `matPolyEquiv` `Polynomial.X` `Matrix.diagonal` `Polynomial.instZero`	—	`Polynomial.eval₂_X` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Matrix.map_one` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `Matrix.smul_one_eq_diagonal`
`matPolyEquiv_symm_apply_coeff` 📖	mathematical	—	`Polynomial.coeff` `CommSemiring.toSemiring` `DFunLike.coe` `AlgEquiv` `Polynomial` `Matrix` `Matrix.semiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Matrix.instAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `AlgEquiv.symm` `matPolyEquiv`	—	`AlgEquiv.apply_symm_apply` `matPolyEquiv_coeff_apply`
`matPolyEquiv_symm_map_eval` 📖	mathematical	—	`Matrix.map` `Polynomial` `CommSemiring.toSemiring` `DFunLike.coe` `AlgEquiv` `Matrix` `Matrix.semiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Matrix.instAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `AlgEquiv.symm` `matPolyEquiv` `Polynomial.eval` `RingHom` `Semiring.toNonAssocSemiring` `Matrix.nonAssocSemiring` `RingHom.instFunLike` `Matrix.scalar`	—	`Commute.symm` `Matrix.scalar_commute` `Commute.all` `Polynomial.algHom_ext'` `AlgHom.ext` `matPolyEquiv_symm_C` `Matrix.map_map` `Polynomial.eval_C` `Matrix.map_id'` `Polynomial.eval₂_C` `matPolyEquiv_symm_X` `Matrix.diagonal_map` `Polynomial.eval_zero` `Polynomial.eval_X` `Polynomial.eval₂_X` `DFunLike.congr_fun`
`support_subset_support_matPolyEquiv` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Polynomial.support` `CommSemiring.toSemiring` `Matrix` `Matrix.semiring` `DFunLike.coe` `AlgEquiv` `Polynomial` `Polynomial.semiring` `Matrix.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `matPolyEquiv`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `matPolyEquiv_coeff_apply` `Matrix.zero_apply`

---

← Back to Index