Documentation Verification Report

MvPolynomial

📁 Source: Mathlib/RingTheory/Algebraic/MvPolynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems `transcendental_X`, `transcendental_polynomial_aeval_X`, `transcendental_polynomial_aeval_X_iff`, `transcendental_supported_X`, `transcendental_supported_X_iff`, `transcendental_supported_polynomial_aeval_X`, `transcendental_supported_polynomial_aeval_X_iff`	7
Total	7

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`transcendental_X` 📖	mathematical	—	`Transcendental` `MvPolynomial` `CommRing.toCommSemiring` `CommRing.toRing` `instCommRingMvPolynomial` `algebra` `Algebra.id` `X`	—	`Polynomial.aeval_X` `transcendental_polynomial_aeval_X` `Polynomial.transcendental_X`
`transcendental_polynomial_aeval_X` 📖	mathematical	`Transcendental` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.ring` `CommRing.toRing` `Polynomial.algebraOfAlgebra` `Algebra.id`	`MvPolynomial` `instCommRingMvPolynomial` `algebra` `DFunLike.coe` `AlgHom` `Polynomial.semiring` `commSemiring` `AlgHom.funLike` `Polynomial.aeval` `X`	—	`transcendental_supported_polynomial_aeval_X` `Set.notMem_empty` `C_injective` `supported_empty` `Transcendental.eq_1` `isAlgebraic_ringHom_iff_of_comp_eq` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass` `RingHom.instRingHomClass` `RingHom.ext` `RingEquivClass.toRingHomClass` `RingHom.id_apply`
`transcendental_polynomial_aeval_X_iff` 📖	mathematical	—	`Transcendental` `MvPolynomial` `CommRing.toCommSemiring` `CommRing.toRing` `instCommRingMvPolynomial` `algebra` `Algebra.id` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `commSemiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.aeval` `X` `Polynomial.ring`	—	`IsAlgebraic.algHom` `transcendental_polynomial_aeval_X`
`transcendental_supported_X` 📖	mathematical	`Set` `Set.instMembership`	`Transcendental` `MvPolynomial` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `supported` `Subalgebra.toCommRing` `instCommRingMvPolynomial` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `X`	—	`Polynomial.aeval_X` `transcendental_supported_polynomial_aeval_X` `Polynomial.transcendental_X`
`transcendental_supported_X_iff` 📖	mathematical	—	`Transcendental` `MvPolynomial` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `supported` `Subalgebra.toCommRing` `instCommRingMvPolynomial` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `X` `Set` `Set.instMembership`	—	`Polynomial.aeval_X` `transcendental_supported_polynomial_aeval_X_iff`
`transcendental_supported_polynomial_aeval_X` 📖	mathematical	`Set` `Set.instMembership` `Transcendental` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.ring` `CommRing.toRing` `Polynomial.algebraOfAlgebra` `Algebra.id`	`MvPolynomial` `Subalgebra` `commSemiring` `algebra` `SetLike.instMembership` `Subalgebra.instSetLike` `supported` `Subalgebra.toCommRing` `instCommRingMvPolynomial` `Subalgebra.toAlgebra` `Ring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial.semiring` `AlgHom.funLike` `Polynomial.aeval` `X`	—	`transcendental_iff_injective` `map_injective` `Polynomial.isScalarTower` `IsScalarTower.right` `Subalgebra.isScalarTower_mid` `isScalarTower` `Subtype.val_injective` `Set.mem_insert` `Polynomial.algHom_ext` `Polynomial.aeval_X` `supportedEquivMvPolynomial_symm_X` `Polynomial.algHom_ext'` `algHom_ext` `Polynomial.aevalTower_C` `rename_X` `aeval_X` `eval₂_X` `aevalTower_X` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Polynomial.map_C` `Polynomial.aeval_C` `AlgHom.algHomClass` `RingHomCompTriple.comp_eq` `RingHomCompTriple.right_ids` `Polynomial.aevalTower_X` `eval₂_C` `aevalTower_C` `rename_polynomial_aeval_X` `AlgHom.restrictScalars.congr_simp` `Polynomial.map_X`
`transcendental_supported_polynomial_aeval_X_iff` 📖	mathematical	—	`Transcendental` `MvPolynomial` `CommRing.toCommSemiring` `Subalgebra` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `supported` `Subalgebra.toCommRing` `instCommRingMvPolynomial` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.aeval` `X` `Set` `Set.instMembership` `Polynomial.ring`	—	`Mathlib.Tactic.Contrapose.contrapose₄` `isAlgebraic_algebraMap` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `nontrivial_of_nontrivial` `Algebra.adjoin_mono` `Set.singleton_subset_iff` `Set.mem_image_of_mem` `Polynomial.aeval_mem_adjoin_singleton` `Transcendental.eq_1` `transcendental_polynomial_aeval_X_iff` `Transcendental.restrictScalars` `Subalgebra.isScalarTower_mid` `isScalarTower` `IsScalarTower.right` `C_injective` `transcendental_supported_polynomial_aeval_X`

---

← Back to Index