Basic

📁 Source: Mathlib/FieldTheory/Minpoly/Basic.lean

Statistics

Metric	Count
Definitions minpoly	1
Theorems aeval, aeval_algHom, aeval_ne_zero_of_dvdNotUnit_minpoly, algEquiv_eq, algHom_eq, algebraMap_eq, degree_eq_one_iff, degree_pos, eq_X_sub_C_of_algebraMap_inj, eq_of_linearIndependent, eq_zero, irreducible, map_ne_one, mem_range_of_degree_eq_one, min, monic, natDegree_eq_one_iff, natDegree_pos, ne_one, ne_zero, ne_zero_iff, not_isUnit, subsingleton, two_le_natDegree_iff, two_le_natDegree_subalgebra, unique'	26
Total	27

(root)

Definitions

Name	Category	Theorems
minpoly 📖	CompOp	208 math math: NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', minpoly.prime_of_isIntegrallyClosed, minpoly.ToAdjoin.injective, mem_perfectClosure_iff_natSepDegree_eq_one, IntermediateField.aeval_gen_minpoly, minpoly.unique, IsPurelyInseparable.minpoly_natDegree_eq', AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, IntermediateField.adjoin.finrank, IsPurelyInseparable.minpoly_eq', AdjoinRoot.minpoly_root, eval_minpolyDiv_self, IsPrimitiveRoot.totient_le_degree_minpoly, eval₂_minpolyDiv_self, isConjRoot_iff_mem_minpoly_aroots, IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen, IsPrimitiveRoot.minpoly_dvd_pow_mod, Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly, minpoly.monic, natDegree_minpolyDiv_succ, minpoly.eq_iff_aeval_eq_zero, sum_smul_minpolyDiv_eq_X_pow, minpoly.eq_of_irreducible, Normal.splits', PowerBasis.quotientEquivQuotientMinpolyMap_apply, Normal.minpoly_eq_iff_mem_orbit, minpoly_algHom_toLinearMap, PowerBasis.ofAdjoinEqTop'_dim, minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C, isConjRoot_def, minpoly.coeff_zero_eq_zero, IsPrimitiveRoot.is_roots_of_minpoly, minpoly.degree_pos, IsPrimitiveRoot.powerBasis_dim, AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, AdjoinRoot.Minpoly.toAdjoin.surjective, Matrix.minpoly_dvd_charpoly, IsNormalClosure.adjoin_rootSet, IntermediateField.minpoly_gen, normalClosure_eq_iSup_adjoin', Algebra.discr_powerBasis_eq_norm, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, Normal.splits, minpoly.sub_algebraMap, isConjRoot_iff_aeval_eq_zero, IsPrimitiveRoot.minpoly_eq_pow_coprime, solvableByRad.isSolvable, IsPurelyInseparable.minpoly_eq, minpoly.degree_le, IsPurelyInseparable.natSepDegree_eq_one, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow, IsNormalClosure.splits, minpoly.two_le_natDegree_iff, minpoly.map_eq_of_isSeparable_of_isPurelyInseparable, minpoly.frobenius_of_isSeparable, charpoly_leftMulMatrix, minpoly.dvd_iff, LinearMap.minpoly_toMatrix', Algebra.adjoin.powerBasis_dim, minpoly.algEquiv_eq, PowerBasis.liftEquiv_symm_apply, ConjRootClass.minpoly_mk, natDegree_minpolyDiv_lt, minpoly.isIntegrallyClosed_eq_field_fractions, AdjoinRoot.Minpoly.coe_toAdjoin, traceForm_dualSubmodule_adjoin, IsIntegrallyClosed.minpoly.unique, minpoly.eq_X_sub_C_of_algebraMap_inj, spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots, LinearMap.minpoly_dvd_charpoly, PowerBasis.trace_gen_eq_nextCoeff_minpoly, minpoly.degree_le_of_ne_zero, isConjRoot_iff_mem_minpoly_rootSet, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp, trace_eq_finrank_mul_minpoly_nextCoeff, minpoly.algHom_eq, PowerBasis.degree_minpoly, IntermediateField.exists_finset_of_mem_supr'', Algebra.adjoin.powerBasis'_dim, minpoly.ker_aeval_eq_span_minpoly, IsPrimitiveRoot.minpoly_dvd_expand, minpoly.eq_of_irreducible_of_monic, minpoly.isRadical, minpoly.prime, IsPrimitiveRoot.minpoly_dvd_mod_p, minpoly.aeval, isPurelyInseparable_iff_natSepDegree_eq_one, IsPrimitiveRoot.separable_minpoly_mod, minpoly.eq_of_linearIndependent, LinearMap.hasEigenvalue_zero_tfae, Matrix.minpoly_toLin', IntermediateField.adjoinRootEquivAdjoin_apply_root, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, minpoly.dvd_map_of_isScalarTower, Module.End.isRoot_of_hasEigenvalue, minpoly.isIntegrallyClosed_dvd_iff, LinearMap.minpoly_toMatrix, minpoly.subsingleton, Algebra.IsUnramifiedAt.not_minpoly_sq_dvd, isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow, minpoly.eq_zero, IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, IsPrimitiveRoot.subOnePowerBasis_dim, minpoly.aeval_algHom, minpoly.IsIntegrallyClosed.degree_le_of_ne_zero, IsPurelyInseparable.minpoly_natDegree_eq, minpoly.add_algebraMap, Algebra.IsAlgebraic.isNormalClosure_iff, IsConjRoot.aeval_eq_zero, IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen, isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, Polynomial.cyclotomic_eq_minpoly_rat, minpoly.min, minpoly.ofSubring, normal_iff, IsPrimitiveRoot.squarefree_minpoly_mod, Field.primitive_element_iff_minpoly_degree_eq, minpoly.dvd_map_of_isScalarTower', PowerBasis.ofGenMemAdjoin'_dim, Polynomial.span_minpoly_eq_annihilator, NumberField.Embeddings.coeff_bdd_of_norm_le, IsIntegral.mem_span_pow, spectralNorm.spectralNorm_eq_norm_coeff_zero_rpow, Algebra.normalizedTrace_minpoly, minpoly.eq_X_sub_C', Field.primitive_element_iff_minpoly_natDegree_eq, coeff_minpolyDiv, IntermediateField.minpoly_eq, minpoly.degree_eq_one_iff, aeval_derivative_mem_differentIdeal, PowerBasis.minpolyGen_eq, IsPurelyInseparable.minpoly_eq_X_pow_sub_C, minpoly.isIntegrallyClosed_dvd, FiniteField.minpoly_frobeniusAlgHom, minpoly.equivAdjoin_toAlgHom, Module.End.hasEigenvalue_iff_isRoot, minpoly_algEquiv_toLinearMap, minpoly.natSepDegree_eq_one_iff_pow_mem, minpoly.zero, minpoly.one, minpoly.neg, normalClosure_eq_iSup_adjoin, IsAdjoinRoot.mkOfAdjoinEqTop_root, IsPurelyInseparable.minpoly_eq_X_sub_C_pow, minpoly.not_isUnit, NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd, IsIntegrallyClosed.minpoly_smul, minpolyDiv_spec, PowerBasis.liftEquiv'_apply_coe, minpoly.coe_equivAdjoin, Algebra.adjoin.powerBasis'_minpoly_gen, minpoly.natDegree_le, PowerBasis.ofAdjoinEqTop_dim, AdjoinRoot.minpoly_powerBasis_gen, Module.End.IsSemisimple.minpoly_squarefree, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, Normal.out, minpoly.dvd, FixedPoints.minpoly_eq_minpoly, conductor_mul_differentIdeal, minpoly.eq_iff_aeval_minpoly_eq_zero, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, minpoly.natDegree_eq_one_iff, IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element, IsPrimitiveRoot.pow_isRoot_minpoly, PowerBasis.liftEquiv'_symm_apply_apply, Polynomial.annIdealGenerator_eq_minpoly, minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C, Module.Basis.traceDual_powerBasis_eq, minpoly.iterateFrobenius_of_isSeparable, LinearMap.not_hasEigenvalue_zero_tfae, Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly, minpoly.degree_dvd, linearIndependent_pow, IsPrimitiveRoot.minpoly_eq_pow, NumberField.Embeddings.range_eval_eq_rootSet_minpoly, minpoly.irreducible, minpoly.algebraMap_eq, minpoly.natDegree_pos, PowerBasis.natDegree_minpoly, IsPrimitiveRoot.minpoly_dvd_cyclotomic, NumberField.RingOfIntegers.minpoly_coe, IsAdjoinRootMonic.minpoly_eq, Polynomial.cyclotomic_eq_minpoly, Matrix.minpoly_toLin, AdjoinRoot.minpoly_powerBasis_gen_of_monic, IsGalois.splits, minpoly.ker_eval, minpoly.eq_X_sub_C, IntermediateField.isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one, minpoly.map_eq_of_equiv_equiv, Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin, Valuation.coeff_zero_minpoly, trace_adjoinSimpleGen, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, minpoly.unique', IntermediateField.adjoin.powerBasis_dim, minpoly.two_le_natDegree_subalgebra, minpoly.isIntegrallyClosed_eq_field_fractions', natDegree_minpolyDiv, PowerBasis.liftEquiv_apply_coe, IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply

minpoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Polynomial.degree_lt_wf WellFounded.min_mem Polynomial.aeval_zero
aeval_algHom 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Polynomial.aeval_algHom AlgHom.coe_comp aeval map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
aeval_ne_zero_of_dvdNotUnit_minpoly 📖	—	IsIntegral Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring DvdNotUnit Polynomial CommSemiring.toCommMonoidWithZero Polynomial.commSemiring minpoly	—	—	LE.le.not_gt min Polynomial.degree_lt_degree Polynomial.Monic.of_mul_monic_left monic Polynomial.Monic.natDegree_mul lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid lt_of_not_ge Polynomial.eq_C_of_natDegree_le_zero Polynomial.leadingCoeff.eq_1 Polynomial.Monic.leadingCoeff Polynomial.C_1 isUnit_one
algEquiv_eq 📖	mathematical	—	minpoly DFunLike.coe AlgEquiv CommRing.toCommSemiring Ring.toSemiring AlgEquiv.instFunLike	—	algHom_eq AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.injective
algHom_eq 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	minpoly	—	isIntegral_algHom_iff Polynomial.aeval_algHom WellFounded.min.congr_simp map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
algebraMap_eq 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring RingHom.instFunLike algebraMap	minpoly CommRing.toRing	—	algHom_eq
degree_eq_one_iff 📖	mathematical	—	Polynomial.degree CommSemiring.toSemiring CommRing.toCommSemiring minpoly WithBot WithBot.one Nat.instOne Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap Ring.toSemiring	—	mem_range_of_degree_eq_one LE.le.antisymm min Polynomial.monic_X_sub_C Polynomial.aeval_sub Polynomial.aeval_X Polynomial.aeval_C sub_self Polynomial.degree_X_sub_C Module.nontrivial Nat.WithBot.add_one_le_of_lt degree_pos isIntegral_algebraMap
degree_pos 📖	mathematical	IsIntegral	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass Polynomial.degree CommSemiring.toSemiring CommRing.toCommSemiring minpoly	—	Polynomial.natDegree_pos_iff_degree_pos natDegree_pos
eq_X_sub_C_of_algebraMap_inj 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring RingHom.instFunLike algebraMap	minpoly Polynomial Polynomial.instSub CommRing.toRing Polynomial.X Polynomial.semiring Polynomial.C	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton unique' Polynomial.monic_X_sub_C map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Polynomial.aeval_C Polynomial.aeval_X sub_self Polynomial.eq_C_of_natDegree_eq_zero Polynomial.natDegree_X_sub_C Polynomial.natDegree_lt_natDegree_iff map_ne_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.C_ne_zero
eq_of_linearIndependent 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom Polynomial Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Polynomial.degree WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne LinearIndependent Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule	minpoly	—	unique' Polynomial.ext lt_or_ge Fintype.linearIndependent_iff Finset.sum_congr Algebra.smul_def Finset.sum_range map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Polynomial.aeval_monomial Polynomial.as_sum_range' Polynomial.natDegree_lt_iff_degree_lt Polynomial.coeff_eq_zero_of_degree_lt LT.lt.trans_le WithBot.coe_le_coe
eq_zero 📖	mathematical	IsIntegral	minpoly Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero	—	—
irreducible 📖	mathematical	IsIntegral	Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring minpoly	—	Polynomial.irreducible_of_monic IsDomain.to_noZeroDivisors monic ne_one IsDomain.toNontrivial Polynomial.Monic.isUnit_iff mul_eq_zero Polynomial.aeval_mul aeval aeval_ne_zero_of_dvdNotUnit_minpoly Polynomial.Monic.ne_zero mul_comm
map_ne_one 📖	—	—	—	—	Polynomial.Monic.eq_one_of_map_eq_one monic ne_one eq_zero Polynomial.map_zero zero_ne_one NeZero.one Polynomial.nontrivial
mem_range_of_degree_eq_one 📖	mathematical	Polynomial.degree CommSemiring.toSemiring CommRing.toCommSemiring minpoly WithBot WithBot.one Nat.instOne	Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap Ring.toSemiring	—	ne_of_lt WithBot.bot_lt_coe WithBot.coe_one Polynomial.degree_zero eq_zero aeval map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass eq_neg_iff_add_eq_zero Polynomial.aeval_X Polynomial.aeval_C Polynomial.aeval_add one_mul Polynomial.C_1 Polynomial.Monic.leadingCoeff monic Polynomial.eq_X_add_C_of_degree_eq_one
min 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom Polynomial Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree minpoly	—	le_of_not_gt WellFounded.not_lt_min Polynomial.degree_lt_wf
monic 📖	mathematical	IsIntegral	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring minpoly	—	Polynomial.degree_lt_wf WellFounded.min_mem
natDegree_eq_one_iff 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring minpoly Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap Ring.toSemiring	—	Polynomial.degree_eq_iff_natDegree_eq_of_pos zero_lt_one Nat.instZeroLEOneClass degree_eq_one_iff
natDegree_pos 📖	mathematical	IsIntegral	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring minpoly	—	pos_iff_ne_zero Nat.instCanonicallyOrderedAdd Polynomial.eq_C_of_natDegree_eq_zero Polynomial.Monic.leadingCoeff monic Polynomial.C_1 map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass NeZero.one aeval
ne_one 📖	—	—	—	—	one_ne_zero NeZero.one aeval map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
ne_zero 📖	—	IsIntegral	—	—	Polynomial.Monic.ne_zero monic
ne_zero_iff 📖	mathematical	—	IsIntegral	—	of_not_not Function.mt eq_zero ne_zero
not_isUnit 📖	mathematical	—	IsUnit Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring minpoly	—	Polynomial.Monic.eq_one_of_isUnit monic ne_one eq_zero not_isUnit_zero Polynomial.nontrivial RingHom.domain_nontrivial
subsingleton 📖	mathematical	—	minpoly Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instOne	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton min Polynomial.monic_one le_or_gt Polynomial.Monic.degree_le_zero_iff_eq_one monic Polynomial.eval₂_one LE.le.not_gt Polynomial.degree_one
two_le_natDegree_iff 📖	mathematical	IsIntegral	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring minpoly Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap Ring.toSemiring	—	iff_not_comm natDegree_eq_one_iff not_le Eq.trans_lt one_lt_two Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Nat.cast_one Nat.cast_zero natDegree_pos Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add
two_le_natDegree_subalgebra 📖	mathematical	IsIntegral Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommRing CommRing.toRing Subalgebra.toAlgebra Ring.toSemiring Algebra.id	Polynomial.natDegree minpoly	—	two_le_natDegree_iff Iff.not Set.ext_iff Subtype.range_val_subtype
unique' 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom Polynomial Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Polynomial.instZero	minpoly	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton Polynomial.degree_modByMonic_lt Polynomial.modByMonic_eq_zero_iff_dvd ne_zero MulZeroClass.mul_zero Polynomial.Monic.leadingCoeff monic Polynomial.leadingCoeff_mul_monic mul_comm add_zero Eq.trans_le Polynomial.Monic.natDegree_mul' Polynomial.natDegree_le_natDegree min Polynomial.eq_C_of_natDegree_le_zero Polynomial.leadingCoeff.eq_1 Polynomial.C_1 mul_one Polynomial.aeval_modByMonic_eq_self_of_root aeval

---

← Back to Index