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 AddMonoidAlgebra.ring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toRing Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra CommSemiring.toSemiring 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	Transcendental MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.ring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toRing Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra CommSemiring.toSemiring Algebra.id DFunLike.coe AlgHom Polynomial Polynomial.semiring AddMonoidAlgebra.semiring Polynomial.algebraOfAlgebra 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 AddMonoidAlgebra.ring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toRing Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra CommSemiring.toSemiring Algebra.id DFunLike.coe AlgHom Polynomial Polynomial.semiring AddMonoidAlgebra.semiring 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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike supported Subalgebra.toCommRing AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.ring CommRing.toRing Subalgebra.toAlgebra AddMonoidAlgebra.commSemiring Ring.toSemiring X	—	Polynomial.aeval_X transcendental_supported_polynomial_aeval_X Polynomial.transcendental_X
transcendental_supported_X_iff 📖	mathematical	—	Transcendental MvPolynomial CommRing.toCommSemiring Subalgebra AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike supported Subalgebra.toCommRing AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.ring CommRing.toRing Subalgebra.toAlgebra AddMonoidAlgebra.commSemiring 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	Transcendental MvPolynomial CommRing.toCommSemiring Subalgebra AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike supported Subalgebra.toCommRing AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.ring CommRing.toRing Subalgebra.toAlgebra AddMonoidAlgebra.commSemiring Ring.toSemiring DFunLike.coe AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra AlgHom.funLike Polynomial.aeval X	—	transcendental_iff_injective map_injective Polynomial.isScalarTower IsScalarTower.right Subalgebra.isScalarTower_mid 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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike supported Subalgebra.toCommRing AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.ring CommRing.toRing Subalgebra.toAlgebra AddMonoidAlgebra.commSemiring 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.right C_injective transcendental_supported_polynomial_aeval_X

---

← Back to Index