Polynomial

📁 Source: Mathlib/RingTheory/Adjoin/Polynomial.lean

Statistics

Metric	Count
Definitions instCommRingAdjoinSingleton, instCommSemiringAdjoinSingleton	2
Theorems adjoin_eq_exists_aeval, adjoin_mem_exists_aeval, adjoin_singleton_eq_range_aeval, adjoin_singleton_induction, adjoin_X, aeval_mem_adjoin_singleton	6
Total	8

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_eq_exists_aeval 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra id AlgHom.funLike Polynomial.aeval Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet	—	adjoin_singleton_eq_range_aeval
adjoin_mem_exists_aeval 📖	mathematical	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra id AlgHom.funLike Polynomial.aeval	—	adjoin_singleton_eq_range_aeval
adjoin_singleton_eq_range_aeval 📖	mathematical	—	adjoin Set Set.instSingletonSet AlgHom.range Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra id Polynomial.aeval	—	map_top Polynomial.adjoin_X AlgHom.map_adjoin Set.image_singleton Polynomial.aeval_X
adjoin_singleton_induction 📖	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra id AlgHom.funLike Polynomial.aeval Polynomial.aeval_mem_adjoin_singleton	—	—	Polynomial.aeval_mem_adjoin_singleton adjoin_eq_exists_aeval

Polynomial

Definitions

Name	Category	Theorems
instCommRingAdjoinSingleton 📖	CompOp	9 math math: Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, Algebra.finite_adjoin_simple_of_isIntegral, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, AdjoinRoot.Minpoly.coe_toAdjoin, quotAdjoinEquivQuotMap_apply_mk, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, IsPrimitiveRoot.adjoin_isCyclotomicExtension
instCommSemiringAdjoinSingleton 📖	CompOp	7 math math: Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow, prod_mem_ideal_map_of_mem_conductor, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime, Algebra.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap, IntermediateField.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_X 📖	mathematical	—	Algebra.adjoin Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id Set Set.instSingletonSet X Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique sum_monomial_eq Subalgebra.sum_mem Subalgebra.smul_mem Subalgebra.pow_mem Algebra.subset_adjoin
aeval_mem_adjoin_singleton 📖	mathematical	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval	—	Algebra.adjoin_singleton_eq_range_aeval

---

← Back to Index