IsIntegral

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

Statistics

Metric	Count
Definitions IsIntegral, IsIntegral, IsIntegral, IsIntegral, IsIntegral	5
Theorems coeff, coeff, coeff_of_exists_smul_mem_lifts, coeff_of_isFractionRing, of_aeval_monic_of_isIntegral_coeff, isIntegral_iff_isIntegral_coeff, isIntegral_coeff_of_dvd, isIntegral_coeff_of_factors, isIntegral_coeff_prod, isIntegral_iff_isIntegral_coeff, instIsIntegrallyClosedPolynomialOfIsDomain	11
Total	16

Algebra

Definitions

Name	Category	Theorems
IsIntegral 📖	CompData	40 math math: IsPushout.isIntegral', IsIntegral.tower_top, IsIntegralClosure.isIntegral_algebra, IsGaloisGroup.iff_isFractionRing, IsIntegral.tensorProduct, integralClosure.AlgebraIsIntegral, IsPurelyInseparable.isIntegral, IsIntegral.adjoin, isIntegral_def, integralClosure_eq_top_iff, instIsIntegralPolynomial, IsIntegral.trans, IsIntegral.of_surjective, IsIntegral.prod, instIsIntegralMvPolynomial, algebraMap_isIntegral_iff, NumberField.RingOfIntegers.extension_algebra_isIntegral, isAlgebraic_iff_isIntegral, IsIntegral.of_injective, IsCyclotomicExtension.integral, IsIntegral.tower_bot, AlgEquiv.isIntegral_iff, isIntegral_of_surjective, le_integralClosure_iff_isIntegral, IsIntegral.of_finite, instIsIntegralQuotientIdeal, isIntegral_iSup, isIntegral_sup, Ideal.Quotient.algebra_isIntegral_of_liesOver, Module.End.isIntegral, NumberField.RingOfIntegers.instIsIntegralInt, IsIntegral.quotient, Subalgebra.isIntegral_iff, finite_iff_isIntegral_and_finiteType, IsPushout.isIntegral, IsInvariant.isIntegral, instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, IsInvariant.isIntegral_of_profinite, isIntegral_iff, IsAlgebraic.isIntegral

AlgebraicGeometry

Definitions

Name	Category	Theorems
IsIntegral 📖	CompData	17 math math: instIsIntegralFiberOfGeometricallyIntegral, IsIntegral.of_isIso, isIntegral_of_irreducibleSpace_of_isReduced, affine_isIntegral_iff, instIsIntegralToSchemeOfNonemptyCarrierCarrierCommRingCat, geometricallyIntegral_iff, GeometricallyIntegral.isIntegral_of_isLocallyNoetherian, isIntegral_iff_irreducibleSpace_and_isReduced, instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1, isIntegral_of_isOpenImmersion, GeometricallyIntegral.isIntegral_of_subsingleton, instIsIntegralSpecOfIsDomainCarrier, instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian, GeometricallyIntegral.eq_geometrically, GeometricallyIntegral.geometrically_isIntegral, Scheme.Hom.instIsIntegralNormalization, isIntegral_of_isAffine_of_isDomain

IsAlmostIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff 📖	mathematical	IsAlmostIntegral Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing Polynomial.algebra	IsAlmostIntegral Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring	—	IsDomain.to_noZeroDivisors IsDomain.toNontrivial Polynomial.instNoZeroDivisors Polynomial.nontrivial Algebra.smul_def AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass Subring.instSubringClass MulZeroClass.mul_zero Polynomial.leadingCoeff_map_of_injective FaithfulSMul.algebraMap_injective Polynomial.leadingCoeff_pow' Polynomial.leadingCoeff_mul' Nat.strong_induction_on Polynomial.natDegree_eq_zero Polynomial.coeff_C Polynomial.leadingCoeff_C Subalgebra.zero_mem Polynomial.self_sub_monomial_natDegree_leadingCoeff mem_completeIntegralClosure Polynomial.C_mul_X_pow_eq_monomial Polynomial.map_X Polynomial.map_pow sub_mem SubringClass.addSubgroupClass Subalgebra.instSubringClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass Subalgebra.instSubsemiringClass Polynomial.map_C map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSMulMemClass Polynomial.eraseLead_coeff_of_ne LE.le.trans_lt Polynomial.eraseLead_natDegree_le

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff 📖	mathematical	IsIntegral Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing Polynomial.ring CommRing.toRing Polynomial.algebra	IsIntegral CommRing.toRing Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite isNoetherian_of_subsingleton isNoetherian_of_finite Finite.of_subsingleton eq_or_ne LE.le.trans_lt Finset.le_sup IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd Polynomial.eval_eq_sum_range Finset.sum_range_succ Polynomial.Monic.add_of_right Polynomial.Monic.leadingCoeff minpoly.monic one_mul Polynomial.degree_lt_degree Polynomial.natDegree_sum_le instCommutativeMax instAssociativeMax Finset.fold_max_lt IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE minpoly.natDegree_pos Polynomial.nontrivial pow_mul lt_imp_lt_of_le_of_le Polynomial.natDegree_mul_le le_refl Polynomial.natDegree_X_pow mul_le_mul_right Nat.instMulLeftMono Polynomial.map_X Polynomial.map_taylor map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass sub_add_cancel Polynomial.eval_map_algebraMap minpoly.aeval Polynomial.taylor_eval Polynomial.coe_aeval_eq_eval Polynomial.aeval_algHom_apply AlgHom.algHomClass neg_dvd neg_sub Polynomial.taylor_coeff_zero Polynomial.IsRoot.dvd_coeff_zero neg Polynomial.isIntegral_coeff_of_dvd Polynomial.Monic.sub_of_left Polynomial.monic_X_pow Polynomial.degree_X_pow le_or_gt Polynomial.coeff_sub Polynomial.coeff_X_pow zero_sub neg_neg Polynomial.coeff_eq_zero_of_natDegree_lt
coeff_of_exists_smul_mem_lifts 📖	mathematical	IsIntegral Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing Polynomial.ring CommRing.toRing Polynomial.algebra	IsIntegral CommRing.toRing Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring	—	coeff
coeff_of_isFractionRing 📖	mathematical	IsIntegral Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing Polynomial.ring CommRing.toRing Polynomial.algebra	IsIntegral CommRing.toRing Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring	—	coeff
of_aeval_monic_of_isIntegral_coeff 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring IsIntegral CommRing.toRing Polynomial.eval Polynomial.coeff	IsIntegral CommRing.toRing	—	Polynomial.lifts_and_natDegree_eq_and_monic Polynomial.lifts_iff_coeff_lifts Subalgebra.setRange_algebraMap isIntegral_trans IsScalarTower.subalgebra' IsScalarTower.right integralClosure.AlgebraIsIntegral of_aeval_monic tower_top

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral_iff_isIntegral_coeff 📖	mathematical	—	IsIntegral MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.ring CommRing.toRing Finsupp.instAddMonoid Nat.instAddMonoid algebraMvPolynomial coeff	—	Finite.induction_empty_option RingHom.IsIntegralElem.of_map rename_injective Equiv.injective RingHom.IsIntegralElem.of_comp ringHom_ext' AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.ext ext algHom_C map_C coeff_C rename_X map_X Equiv.apply_symm_apply rename_rename Equiv.self_comp_symm rename_id Finsupp.embDomain_eq_mapDomain coeff_rename_mapDomain PEmpty.instIsEmpty AlgEquiv.injective AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgHom.map_algebraMap IsScalarTower.right AddMonoidAlgebra.isScalarTower aeval_X constantCoeff_comp_C eval_C constantCoeff_X eval_X AlgEquiv.symm_apply_apply Finsupp.instSubsingleton IsIntegral.coeff optionEquivLeft_C Polynomial.map_C optionEquivLeft_symm_C_C optionEquivLeft_X_none Polynomial.map_X optionEquivLeft_symm_X optionEquivLeft_X_some optionEquivLeft_symm_C_X optionEquivLeft_coeff_some_coeff_none exists_rename_eq_of_vars_subset_range Subtype.val_injective Subtype.range_coe_subtype Set.instReflSubset killCompl_map killCompl_rename_app RingHom.IsIntegralElem.map Finite.of_fintype coeff_rename_eq_zero isIntegral_zero support_sum_monomial_coeff Finset.sum_congr monomial_eq IsIntegral.sum IsIntegral.mul IsIntegral.tower_top instIsScalarTower IsIntegral.map IsIntegral.prod IsIntegral.pow isIntegral_algebraMap

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral_coeff_of_dvd 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing map algebraMap	IsIntegral CommRing.toRing coeff CommSemiring.toSemiring CommRing.toCommSemiring	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Module.IsNoetherian.finite isNoetherian_of_finite Finite.of_subsingleton Monic.exists_splits_map IsScalarTower.of_algebraMap_eq' isIntegral_algHom_iff FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial IsScalarTower.coe_toAlgHom' coeff_map isIntegral_coeff_of_factors Monic.leadingCoeff Monic.map aeval_map_algebraMap aeval_eq_zero_of_dvd_aeval_eq_zero eval_map_algebraMap
isIntegral_coeff_of_factors 📖	mathematical	IsIntegral CommRing.toRing leadingCoeff CommSemiring.toSemiring CommRing.toCommSemiring Splits	IsIntegral CommRing.toRing coeff CommSemiring.toSemiring CommRing.toCommSemiring	—	splits_iff_exists_multiset Multiset.prod_eq_prod_coe coeff_C_mul IsIntegral.mul isIntegral_coeff_prod IsRoot.eq_1 eval_mul eval_multiset_prod Multiset.prod_eq_zero Multiset.map_map Multiset.map_congr eval_sub eval_X eval_C MulZeroClass.mul_zero Multiset.mem_map Multiset.count_pos LE.le.trans_lt coeff_sub coeff_X coeff_C
isIntegral_coeff_prod 📖	mathematical	IsIntegral CommRing.toRing coeff CommSemiring.toSemiring CommRing.toCommSemiring	IsIntegral CommRing.toRing coeff CommSemiring.toSemiring CommRing.toCommSemiring Finset.prod Polynomial CommRing.toCommMonoid commRing	—	Finset.induction coeff_one Finset.prod_insert coeff_mul IsIntegral.sum IsIntegral.mul
isIntegral_iff_isIntegral_coeff 📖	mathematical	—	IsIntegral Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commRing ring CommRing.toRing algebra coeff	—	IsIntegral.coeff sum_monomial_eq sum.eq_1 Finset.sum_congr map_X IsIntegral.sum IsIntegral.mul IsIntegral.tower_top instIsScalarTowerPolynomial IsScalarTower.left IsIntegral.map isScalarTower AlgHom.algHomClass IsIntegral.pow isIntegral_algebraMap

RingHom

Definitions

Name	Category	Theorems
IsIntegral 📖	MathDef	32 math math: IsIntegral.tower_bot, isIntegral_localization, AlgebraicGeometry.IsIntegralHom.isIntegral_app, Polynomial.Monic.quotient_isIntegral, IsIntegral.tower_top, isIntegral_respectsIso, algebraMap_isIntegral_iff, isIntegral_isStableUnderBaseChange, isIntegral_localization', AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, isIntegral_ofLocalizationSpan, IsIntegral.of_finite, exists_integral_inj_algHom_of_quotient, isIntegral_of_surjective, Finite.to_isIntegral, Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, IsIntegral.quotient, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.isIntegralHom_iff, IsIntegral.trans, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.IsIntegralHom.SpecMap_iff, finite_iff_isIntegral_and_finiteType, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom, MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing, isIntegral_quotientMap_iff, exists_integral_inj_algHom_of_fg, isIntegral_stableUnderComposition, Polynomial.comp_C_integral_of_surjective_of_isJacobsonRing, Polynomial.isIntegral_isLocalization_polynomial_quotient

WeierstrassCurve

Definitions

Name	Category	Theorems
IsIntegral 📖	CompData	6 math math: IsMinimal.val_Δ_maximal, isMinimal_iff, exists_isIntegral, isIntegral_iff, instIsIntegralOfIsMinimal, isIntegral_of_exists_lift

(root)

Definitions

Name	Category	Theorems
IsIntegral 📖	MathDef	145 math math: exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range, IsIntegral.of_mem_closure, IsIntegrallyClosedIn.isIntegral_iff, Algebra.IsIntegral.isIntegral, Polynomial.isIntegral_coeff_prod, IsIntegrallyClosed.isIntegral_iff, PowerBasis.repr_pow_isIntegral, isIntegral_of_smul_mem_submodule, IsIntegral.of_neg, IsIntegral.pair, Algebra.isIntegral_def, Real.isIntegral_two_mul_sin_rat_mul_pi, PowerBasis.isIntegral_gen, minpoly.ne_zero_iff, isIntegral_of_noetherian, Algebra.IsAlgebraic.exists_integral_multiples, Algebra.zariskisMainProperty_iff, IsAlmostIntegral.isIntegral, IsIntegral.mul, Algebra.isIntegral_trace, Real.isIntegral_two_mul_cos_rat_mul_pi, IsPurelyInseparable.isIntegral', IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap, IsIntegral.exists_multiple_integral_of_isLocalization, IsIntegral.tower_bot, IsAlmostIntegral.isIntegral_of_nonZeroDivisors_le_comap, IsIntegralClosure.isIntegral_iff, isIntegral_algHom_iff, isAlmostIntegral_iff_isIntegral, IsIntegral.multiset_sum, IsIntegral.of_mul_unit, IsLocalization.Away.isIntegral_of_isIntegral_map, IsIntegral.ratCast_iff, minpoly.IsIntegrallyClosed.isIntegral_iff_leadingCoeff_dvd, Complex.isIntegral_exp_rat_mul_pi_mul_I, isIntegral_trans, IsIntegral.of_pow, exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range, IsIntegral.add, IsAlgebraic.exists_integral_multiple, Algebra.zariskisMainProperty_iff', IsIntegral.sub, isIntegral_of_isIntegral_adjoin_of_mul_eq_one, Valuation.Integers.isIntegral_iff_v_le_one, PowerBasis.repr_gen_pow_isIntegral, IsIntegral.of_mem_closure', IntermediateField.coe_isIntegral_iff, IsIntegral.pow, IsIntegralClosure.isIntegral, IsIntegral.pair_iff, IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_mk', IsIntegral.multiset_prod, IsIntegral.coeff, IsLocalization.exists_isIntegral_smul_of_isIntegral_map, isIntegral_algebraMap, IsIntegral.smul, Algebra.zariskisMainProperty_iff_exists_saturation_eq_top, PowerBasis.repr_mul_isIntegral, Polynomial.isIntegral_coeff_of_factors, Complex.isIntegral_two_mul_sin_rat_mul_pi, IsIntegral.prod, map_isIntegral_int, isIntegral_algEquiv, PowerBasis.toMatrix_isIntegral, IsPrimitiveRoot.isIntegral, Algebra.isSeparable_iff, Normal.isIntegral, isIntegral_of_submodule_noetherian, IsAdjoinRootMonic.isIntegral_root, isIntegral_algebraMap_iff, IsIntegral.pow_iff, IsIntegral.det, mem_integralClosure_iff, ValuationSubring.isIntegral_of_mem_ringOfIntegers', Complex.isIntegral_exp_neg_rat_mul_pi_mul_I, NumberField.RingOfIntegers.isIntegral_coe, isIntegral_discr_mul_of_mem_traceDual, FixedPoints.isIntegral, RingEquiv.isIntegral_iff, ValuationSubring.isIntegral_of_mem_ringOfIntegers, normal_iff, IsIntegral.map, AdjoinRoot.isIntegral_root', IsIntegral.neg_iff, IsIntegral.map_of_comp_eq, IsAlgebraic.iff_exists_smul_integral, IsIntegral.of_aeval_monic_of_isIntegral_coeff, isIntegral_iff_isIntegral_closure_finite, isIntegral_of_isIntegralElem_of_monic_of_natDegree_lt, isPurelyInseparable_iff, IsIntegral.nsmul, isIntegral_one, MvPolynomial.isIntegral_iff_isIntegral_coeff, exists_integral_multiples, IsIntegral.neg, exists_derivative_mul_eq_and_isIntegral_coeff, IsAlgebraic.isIntegral, IntermediateField.AdjoinSimple.isIntegral_gen, mem_algebraicClosure_iff', Complex.isIntegral_two_mul_cos_rat_mul_pi, Polynomial.isIntegral_iff_isIntegral_coeff, IsIntegral.tmul, NumberField.RingOfIntegers.isIntegral, IsGalois.integral, FiniteDimensional.exists_is_basis_integral, Algebra.IsSeparable.isIntegral, Normal.out, IsIntegral.tower_top, LinearMap.isIntegral, minpoly.IsIntegrallyClosed.isIntegral_iff_isUnit_leadingCoeff, Polynomial.isIntegral_of_mahlerMeasure_eq_one, IsIntegral.of_mem_of_fg, NumberField.Embeddings.finite_of_norm_le, IsIntegral.inv, integralClosure.isIntegral, IsIntegral.of_finite, Complex.isIntegral_rat_I, solvableByRad.isIntegral, isIntegral_zero, IsIntegral.of_subring, IsIntegral.coeff_of_isFractionRing, IsIntegral.algebraMap, Polynomial.isIntegral_coeff_of_dvd, IsConjRoot.isIntegral, IsIntegral.of_aeval_monic, isIntegral_two_mul_cos_rat_mul_pi, Subalgebra.isIntegral_iff, IsIntegral.coeff_of_exists_smul_mem_lifts, IsConjRoot.isIntegral_iff, Algebra.discr_isIntegral, Algebra.isIntegral_norm, IsIntegral.sum, Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver, Matrix.isIntegral, isAlgebraic_iff_isIntegral, isIntegral_leadingCoeff_smul, Complex.isIntegral_int_I, IsIntegral.zsmul, isIntegral_of_mem_solvableByRad, Submodule.mem_traceDual_iff_isIntegral, IntermediateField.isIntegral_iff, AdjoinRoot.isIntegral_root, Algebra.isIntegral_iff, IsIntegral.tower_bot_of_field, IsSeparable.isIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIntegrallyClosedPolynomialOfIsDomain 📖	mathematical	—	IsIntegrallyClosed Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing	—	UniqueFactorizationMonoid.instIsIntegrallyClosed Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain Polynomial.uniqueFactorizationMonoid PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain isIntegrallyClosedIn_iff Polynomial.map_injective IsFractionRing.injective Localization.isLocalization Polynomial.lifts_iff_coeff_lifts IsIntegrallyClosed.isIntegral_iff IsIntegral.coeff IsIntegrallyClosed.of_isIntegrallyClosed_of_isIntegrallyClosedIn instFaithfulSMulPolynomial FractionRing.instFaithfulSMul Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial

---

← Back to Index