Documentation Verification Report

IsIntegral

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

Statistics

Metric	Count
Definitions	0
Theorems `cyclotomic_comp_X_add_one_isEisensteinAt`, `cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt`, `dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt`, `mem_adjoin_of_dvd_coeff_of_dvd_aeval`, `mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt`, `mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt`	6
Total	6

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cyclotomic_comp_X_add_one_isEisensteinAt` 📖	mathematical	—	`Polynomial.IsEisensteinAt` `Int.instCommSemiring` `Polynomial.comp` `Ring.toSemiring` `Int.instRing` `Polynomial.cyclotomic` `Polynomial` `Polynomial.instAdd` `Polynomial.X` `Polynomial.instOne` `Submodule.span` `Int.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `Set` `Set.instSingletonSet`	—	`Polynomial.Monic.isEisensteinAt_of_mem_of_notMem` `eq_intCast` `RingHom.instRingHomClass` `Int.cast_one` `Polynomial.Monic.comp` `Polynomial.cyclotomic.monic` `Polynomial.monic_X_add_C` `zero_ne_one` `Polynomial.natDegree_X_add_C` `Int.instNontrivial` `Ideal.IsPrime.ne_top` `Ideal.span_singleton_prime` `Nat.cast_zero` `Int.instCharZero` `Nat.Prime.ne_zero` `Fact.out` `Nat.prime_iff_prime_int` `Polynomial.cyclotomic_prime` `Polynomial.geom_sum_X_comp_X_add_one_eq_sum` `Polynomial.lcoeff_apply` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Polynomial.C_eq_natCast` `Polynomial.C_mul_X_pow_eq_monomial` `Polynomial.coeff_monomial` `Finset.sum_ite_eq'` `LT.lt.trans_le` `Nat.totient_prime` `Polynomial.natDegree_cyclotomic` `mul_one` `Polynomial.natDegree_comp` `NormMulClass.toNoZeroDivisors` `Int.instNormMulClass` `Nat.Prime.dvd_choose_self` `lt_tsub_iff_right` `Nat.instOrderedSub` `Polynomial.coeff_zero_eq_eval_zero` `Polynomial.eval_comp` `Polynomial.eval_add` `Polynomial.eval_X` `Polynomial.eval_one` `zero_add` `Polynomial.eval_geom_sum` `one_geom_sum` `Ideal.submodule_span_eq` `IsScalarTower.left` `Ideal.span_singleton_pow` `Ideal.instIsTwoSided_1` `Ideal.mem_span_singleton` `Nat.Prime.two_le` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_congr` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Nat.cast_pow` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Mathlib.Tactic.Linarith.natCast_nonneg`
`cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt` 📖	mathematical	—	`Polynomial.IsEisensteinAt` `Int.instCommSemiring` `Polynomial.comp` `Ring.toSemiring` `Int.instRing` `Polynomial.cyclotomic` `Monoid.toNatPow` `Nat.instMonoid` `Polynomial` `Polynomial.instAdd` `Polynomial.X` `Polynomial.instOne` `Submodule.span` `Int.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `Set` `Set.instSingletonSet`	—	`Polynomial.Monic.isEisensteinAt_of_mem_of_notMem` `eq_intCast` `RingHom.instRingHomClass` `Int.cast_one` `Polynomial.Monic.comp` `Polynomial.cyclotomic.monic` `Polynomial.monic_X_add_C` `zero_ne_one` `Polynomial.natDegree_X_add_C` `Int.instNontrivial` `Ideal.IsPrime.ne_top` `Ideal.span_singleton_prime` `Nat.cast_zero` `Int.instCharZero` `Nat.Prime.ne_zero` `Fact.out` `Nat.prime_iff_prime_int` `pow_one` `Polynomial.IsEisensteinAt.mem` `cyclotomic_comp_X_add_one_isEisensteinAt` `Ideal.submodule_span_eq` `Ideal.mem_span_singleton` `ZMod.intCast_zmod_eq_zero_iff_dvd` `Polynomial.coeff_map` `Polynomial.map_comp` `Polynomial.map_cyclotomic` `Polynomial.map_add` `Polynomial.map_X` `Polynomial.map_one` `pow_add` `Polynomial.cyclotomic_mul_prime_dvd_eq_pow` `ZMod.charP` `pow_succ'` `Polynomial.pow_comp` `ZMod.expand_card` `Polynomial.coeff_expand` `Nat.Prime.pos` `mul_comm` `Nat.totient_prime_pow` `Polynomial.natDegree_cyclotomic` `mul_one` `Polynomial.natDegree_comp` `NormMulClass.toNoZeroDivisors` `Int.instNormMulClass` `lt_of_mul_lt_mul_left'` `contravariant_lt_of_covariant_le` `Nat.instMulLeftMono` `mul_assoc` `Polynomial.coeff_zero_eq_eval_zero` `Polynomial.eval_comp` `Polynomial.cyclotomic_prime_pow_eq_geom_sum` `Polynomial.eval_add` `Polynomial.eval_X` `Polynomial.eval_one` `zero_add` `Polynomial.eval_finset_sum` `Ideal.span_singleton_pow` `Ideal.instIsTwoSided_1` `Finset.sum_congr` `Polynomial.eval_pow` `one_pow` `Finset.sum_const` `Finset.card_range` `Nat.smul_one_eq_cast` `Nat.Prime.two_le` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_congr` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Nat.cast_pow` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `Mathlib.Tactic.Linarith.natCast_nonneg`
`dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt` 📖	mathematical	`Prime` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `PowerBasis.gen` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `Algebra.toSMul` `Polynomial.IsEisensteinAt` `minpoly` `Submodule.span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set` `Set.instSingletonSet`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.coeff`	—	`LT.lt.ne'` `PowerBasis.dim_pos` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `PowerBasis.finrank` `commRing_strongRankCondition` `PowerBasis.natDegree_minpoly` `minpoly.isIntegrallyClosed_eq_field_fractions'` `instIsDomain` `Polynomial.Monic.natDegree_map` `minpoly.monic` `IsIntegral.sub` `IsIntegral.mul` `IsIntegral.pow` `IsIntegral.sum` `IsIntegral.smul` `IsScalarTower.left` `adjoin_le_integralClosure` `IsIntegrallyClosed.isIntegral_iff` `Algebra.isIntegral_norm` `IsFractionRing.injective` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_neg` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `Algebra.smul_def` `IsScalarTower.algebraMap_apply` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `Algebra.norm_algebraMap` `Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly` `Polynomial.coeff_map` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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.pow_prod_atom` `eq_sub_of_add_eq` `pow_add` `smul_smul` `mul_comm` `add_mul` `Distrib.rightDistribClass` `smul_mul_assoc` `IsScalarTower.right` `one_mul` `Finset.sum_mul` `Finset.sum_congr` `pow_zero` `Polynomial.aeval_eq_sum_range` `Finset.add_sum_erase` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `Algebra.smul_mul_assoc` `Polynomial.IsEisensteinAt.notMem` `Ideal.mem_span_singleton` `Ideal.span_singleton_pow` `Ideal.instIsTwoSided_1` `Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd` `IsDomain.toIsCancelMulZero` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `add_zero` `Mathlib.Tactic.RingNF.mul_assoc_rev` `pow_mul` `neg_one_sq` `one_pow` `IsUnit.dvd_mul_right` `Nontrivial.to_nonempty` `Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le` `minpoly.aeval` `Polynomial.IsEisensteinAt.isWeaklyEisensteinAt` `Function.sometimes_spec`
`mem_adjoin_of_dvd_coeff_of_dvd_aeval` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Polynomial.coeff` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `Algebra.toSMul`	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet`	—	`smul_right_injective` `IsDomain.toIsCancelMulZero` `Finset.smul_sum` `Finset.mem_range` `smul_smul` `Finset.sum_range` `Polynomial.aeval_eq_sum_range` `Subalgebra.sum_mem` `Subalgebra.smul_mem` `Subalgebra.pow_mem` `Algebra.subset_adjoin` `Set.mem_singleton` `Nontrivial.to_nonempty` `IsDomain.toNontrivial` `Function.sometimes_spec`
`mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt` 📖	—	`Prime` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `PowerBasis.gen` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subalgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Algebra.toSMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Polynomial.IsEisensteinAt` `minpoly` `Submodule.span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—	`pow_zero` `one_smul` `mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt` `IsIntegral.smul` `IsScalarTower.left` `SemigroupAction.mul_smul` `pow_succ'`
`mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt` 📖	—	`Prime` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `PowerBasis.gen` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subalgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Algebra.toSMul` `Polynomial.IsEisensteinAt` `minpoly` `Submodule.span` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—	`Polynomial.IsEisensteinAt.notMem` `Ideal.mem_span_singleton` `IsScalarTower.left` `Ideal.span_singleton_pow` `Ideal.instIsTwoSided_1` `PowerBasis.finite` `LT.lt.ne'` `PowerBasis.dim_pos` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.IsTorsionFree.trans_faithfulSMul` `IsFractionRing.instFaithfulSMul` `IsDomain.toNontrivial` `IsDomain.toIsCancelMulZero` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.adjoin_singleton_eq_range_aeval` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `minpoly.aeval` `MulZeroClass.zero_mul` `add_zero` `Polynomial.modByMonic_add_div` `minpoly.monic` `Polynomial.aeval_zero` `Algebra.smul_def` `IsDomain.to_noZeroDivisors` `IsScalarTower.algebraMap_eq` `RingHom.injective` `DivisionRing.isSimpleRing` `IsFractionRing.injective` `Prime.ne_zero` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Subalgebra.zero_mem` `mem_adjoin_of_dvd_coeff_of_dvd_aeval` `Nat.case_strong_induction_on` `dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt` `Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd` `Polynomial.degree_modByMonic_lt` `lt_of_lt_of_le` `lt_of_le_of_lt` `Finset.mem_range` `Polynomial.natDegree_lt_natDegree_iff` `add_comm` `add_assoc` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `LT.lt.le` `Finset.mem_range_succ_iff` `le_trans` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_assoc` `smul_mul_assoc` `IsScalarTower.right` `pow_add` `Polynomial.Monic.natDegree_map` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `le_add_iff_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `mul_smul_comm` `Algebra.to_smulCommClass` `Finset.sum_congr` `Finset.sum_union` `Finset.disjoint_range_addLeftEmbedding` `Finset.range_add` `Polynomial.aeval_eq_sum_range` `eq_sub_of_add_eq` `mul_add` `Distrib.leftDistribClass` `Finset.mul_sum` `Finset.sum_insert` `Finset.notMem_erase` `Finset.insert_erase` `tsub_pos_iff_lt` `Finset.sum_mul` `add_mul` `Distrib.rightDistribClass` `Finset.sum_map` `IsIntegral.sub` `IsIntegral.mul` `IsIntegral.pow` `IsIntegral.add` `IsIntegral.sum` `IsIntegral.smul` `adjoin_le_integralClosure` `zero_le` `IsIntegrallyClosed.isIntegral_iff` `Algebra.isIntegral_norm` `dvd_mul_of_dvd_left` `dvd_rfl` `mul_comm` `Units.dvd_mul_left` `Units.val_pow_eq_pow_val` `mul_pow` `Units.coe_neg_one` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_neg` `map_one` `MonoidHomClass.toOneHomClass` `Polynomial.coeff_map` `minpoly.isIntegrallyClosed_eq_field_fractions'` `Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly` `PowerBasis.finrank` `commRing_strongRankCondition` `Algebra.norm_algebraMap` `IsScalarTower.algebraMap_apply` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `mul_sub` `PowerBasis.natDegree_minpoly` `Nontrivial.to_nonempty` `Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le` `Polynomial.IsEisensteinAt.isWeaklyEisensteinAt` `Function.sometimes_spec`

---

← Back to Index