AdjoinRoot

📁 Source: Mathlib/RingTheory/Localization/Away/AdjoinRoot.lean

Statistics

Metric	Count
Definitions AdjoinRoot, awayEquivAdjoin	2
Theorems of_isLocalizationAway, finitePresentation, adjoin_inv, instFinitePresentationAway, instFiniteTypeAway	5
Total	7

Algebra.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isLocalizationAway 📖	mathematical	—	Algebra.FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	—	IsLocalization.Away.finitePresentation trans

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_inv 📖	mathematical	—	Away CommRing.toCommSemiring AdjoinRoot Polynomial CommSemiring.toSemiring Polynomial.instSub CommRing.toRing Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.X Polynomial.instOne AdjoinRoot.instCommRing AdjoinRoot.instAlgebra Algebra.id	—	isLocalization_of_algEquiv Localization.isLocalization

IsLocalization.Away

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finitePresentation 📖	mathematical	—	Algebra.FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	—	Algebra.FinitePresentation.equiv AdjoinRoot.finitePresentation Algebra.FinitePresentation.self Localization.isLocalization

Localization

Definitions

Name	Category	Theorems
awayEquivAdjoin 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
AdjoinRoot 📖	CompOp	144 math math: AdjoinRoot.algEquivOfAssociated_apply_root, minpoly.ToAdjoin.injective, AdjoinRoot.isAdjoinRoot_root_eq_root, AdjoinRoot.instNumberFieldRat, AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, AdjoinRoot.minpoly_root, autAdjoinRootXPowSubCEquiv_root, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, root_X_pow_sub_C_eq_zero_iff, IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen, Polynomial.SplittingFieldAux.succ, IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_eq_mk, PowerBasis.quotientEquivQuotientMinpolyMap_apply, adjoinRootXPowSubCEquiv_symm_eq_root, Polynomial.SplittingFieldAux.algebraMap_succ, AdjoinRoot.mk_surjective, autAdjoinRootXPowSubCEquiv_symm_smul, AdjoinRoot.algEquivOfAssociated_root, AdjoinRoot.algHom_ext_iff, AdjoinRoot.powerBasis'_gen, AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, AdjoinRoot.smul_mk, AdjoinRoot.quotEquivQuotMap_symm_apply_mk, AdjoinRoot.algHom_ext'_iff, AdjoinRoot.liftAlgHom_of, AdjoinRoot.evalEval_apply, AdjoinRoot.symm_mapRingEquiv, AdjoinRoot.Minpoly.toAdjoin.surjective, AdjoinRoot.powerBasis'_dim, Differential.instDifferentialAlgebraAdjoinRoot, AdjoinRoot.instIsNoetherianRing, AdjoinRoot.mk_eq_mk, AdjoinRoot.algHomOfDvd_root, AdjoinRoot.isDomain_of_prime, AdjoinRoot.coe_mapAlgHom, AdjoinRoot.coe_liftHom, AdjoinRoot.algebraMap_eq, AdjoinRoot.mul_div_root_cancel, AdjoinRoot.aeval_eq_of_algebra, AdjoinRoot.mk_leftInverse, AdjoinRoot.algebraMap_eq', Polynomial.natDegree_removeFactor, AdjoinRoot.finiteType, AdjoinRoot.coe_injective, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, IsAdjoinRoot.adjoinRootAlgEquiv_apply_root, AdjoinRoot.mk_eq_zero, AdjoinRoot.Minpoly.coe_toAdjoin, AdjoinRoot.lift_comp_of, AdjoinRoot.quotEquivQuotMap_apply, AdjoinRoot.isAdjoinRoot_map_eq_mkₐ, Polynomial.SplittingFieldAux.scalar_tower', AdjoinRoot.coe_injective', IntermediateField.adjoin_root_eq_top, AdjoinRoot.smul_of, AdjoinRoot.isAlgebraic_root, AdjoinRoot.isScalarTower_right, AdjoinRoot.liftAlgHom_eq_algHom, IsAdjoinRoot.algEquiv_def, Polynomial.Monic.finite_adjoinRoot, AdjoinRoot.lift_mk, AdjoinRoot.root_isInv, IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map, AdjoinRoot.modByMonicHom_mk, AdjoinRoot.isAdjoinRootMonic_toAdjoinRoot, AdjoinRoot.mapAlgHom_comp_mapAlghom, AdjoinRoot.map_comp_map, AdjoinRoot.liftAlgHom_mk, AdjoinRoot.algEquivOfAssociated_toAlgHom, AdjoinRoot.coe_mkₐ, AdjoinRoot.algEquivOfEq_root, AdjoinRoot.instIsScalarTower, IntermediateField.adjoinRootEquivAdjoin_apply_root, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, AdjoinRoot.powerBasisAux'_repr_symm_apply, AdjoinRoot.quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, AdjoinRoot.toRingHom_liftAlgHom, IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk, root_X_pow_sub_C_pow, AdjoinRoot.algEquivOfAssociated_symm, isSplittingField_AdjoinRoot_X_pow_sub_C, AdjoinRoot.toRingHom_ofAlgHom, AdjoinRoot.liftHom_eq_algHom, AdjoinRoot.eval₂_root, IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_root, Polynomial.natDegree_removeFactor', AdjoinRoot.isIntegral_root', AdjoinRoot.algEquivOfEq_apply_root, adjoinRootXPowSubCEquiv_root, AdjoinRoot.coe_liftAlgHom, AdjoinRoot.powerBasis_dim, AdjoinRoot.map_root, AdjoinRoot.noZeroSMulDivisors_of_prime_of_degree_ne_zero, AdjoinRoot.mk_X, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, minpoly.equivAdjoin_toAlgHom, AdjoinRoot.algHom_subsingleton, AdjoinRoot.instSMulCommClass, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, AdjoinRoot.lift_of, AdjoinRoot.coe_mapAlgEquiv, minpoly.coe_equivAdjoin, AdjoinRoot.finitePresentation, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, AdjoinRoot.minpoly_powerBasis_gen, AdjoinRoot.aeval_algHom_eq_zero, AdjoinRoot.lift_root, AdjoinRoot.quotEquivQuotMap_symm_apply, AdjoinRoot.nontrivial, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, AdjoinRoot.powerBasisAux'_repr_apply_to_fun, AdjoinRoot.coe_algEquivOfEq, AdjoinRoot.aeval_eq, IsLocalization.adjoin_inv, AdjoinRoot.liftHom_of, AdjoinRoot.adjoinRoot_eq_top, Polynomial.X_sub_C_mul_removeFactor, AdjoinRoot.map_of, AdjoinRoot.mk_self, AdjoinRoot.liftHom_root, AdjoinRoot.symm_mapAlgEquiv, AdjoinRoot.coe_algHomOfDvd, Polynomial.Monic.free_adjoinRoot, AdjoinRoot.liftAlgHom_root, autAdjoinRootXPowSubC_root, AdjoinRoot.algEquivOfEq_symm, AdjoinRoot.minpoly_powerBasis_gen_of_monic, AdjoinRoot.liftHom_mk, AdjoinRoot.algEquivOfEq_toAlgHom, AdjoinRoot.coe_mapRingEquiv, AdjoinRoot.algHomOfDvd_apply_root, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, WeierstrassCurve.Affine.CoordinateRing.basis_apply, AdjoinRoot.mkₐ_toRingHom, AdjoinRoot.isIntegral_root, AdjoinRoot.ringHom_ext_iff, AdjoinRoot.powerBasis_gen, AdjoinRoot.mk_C, AdjoinRoot.coe_ofAlgHom, AdjoinRoot.of.injective_of_degree_ne_zero, AdjoinRoot.isRoot_root, AdjoinRoot.evalEval_mk, AdjoinRoot.coe_algEquivOfAssociated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFinitePresentationAway 📖	mathematical	—	Algebra.FinitePresentation Localization.Away CommRing.toCommMonoid CommRing.toCommSemiring OreLocalization.instSemiring Ring.toSemiring CommRing.toRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAlgebra	—	Algebra.FinitePresentation.of_isLocalizationAway OreLocalization.instIsScalarTower IsScalarTower.right Localization.isLocalization
instFiniteTypeAway 📖	mathematical	—	Algebra.FiniteType Localization.Away CommRing.toCommMonoid CommRing.toCommSemiring OreLocalization.instSemiring Ring.toSemiring CommRing.toRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAlgebra	—	Algebra.FiniteType.trans OreLocalization.instIsScalarTower IsScalarTower.right Algebra.FiniteType.of_finitePresentation instFinitePresentationAway Algebra.FinitePresentation.self

---

← Back to Index