Eval

📁 Source: Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean

Statistics

Metric	Count
Definitions	0
Theorems cyclotomic_eval_le_add_one_pow_totient, cyclotomic_eval_lt_add_one_pow_totient, cyclotomic_nonneg, cyclotomic_pos, cyclotomic_pos', cyclotomic_pos_and_nonneg, eval_one_cyclotomic_not_prime_pow, eval_one_cyclotomic_prime, eval_one_cyclotomic_prime_pow, eval₂_one_cyclotomic_prime, eval₂_one_cyclotomic_prime_pow, sub_one_lt_natAbs_cyclotomic_eval, sub_one_pow_totient_le_cyclotomic_eval, sub_one_pow_totient_lt_cyclotomic_eval, sub_one_pow_totient_lt_natAbs_cyclotomic_eval	15
Total	15

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cyclotomic_eval_le_add_one_pow_totient 📖	mathematical	Real Real.instLT Real.instOne	Real.instLE eval Ring.toSemiring Real.instRing cyclotomic Monoid.toNatPow Real.instMonoid Real.instAdd Nat.totient	—	cyclotomic_zero eval_one pow_zero cyclotomic_one eval_sub eval_X pow_one AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_assoc IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instZeroLEOneClass cyclotomic_two eval_add Nat.totient_two LT.lt.le cyclotomic_eval_lt_add_one_pow_totient le_add_self Nat.instCanonicallyOrderedAdd
cyclotomic_eval_lt_add_one_pow_totient 📖	mathematical	Real Real.instLT Real.instOne	eval Ring.toSemiring Real.instRing cyclotomic Monoid.toNatPow Real.instMonoid Real.instAdd Nat.totient	—	pos_of_gt Nat.instCanonicallyOrderedAdd LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.one Real.instNontrivial instIsDomain Complex.norm_real Real.norm_of_nonneg LT.lt.le LE.le.trans_lt zero_le_one IsPrimitiveRoot.norm'_eq_one mem_primitiveRoots LT.lt.ne' norm_sub_le Nat.instAtLeastTwoHAddOfNat Complex.isPrimitiveRoot_exp Real.instIsStrictOrderedRing Complex.sameRay_iff Nat.cast_zero neg_ne_zero IsPrimitiveRoot.ne_zero Complex.instNontrivial Complex.arg_ofReal_of_nonneg IsPrimitiveRoot.unique IsPrimitiveRoot.zero neg_eq_zero Complex.neg_im neg_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Complex.neg_re Complex.arg_eq_zero_iff LE.le.lt_of_ne Mathlib.Tactic.Contrapose.contrapose₄ Complex.ext 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.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 Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq 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 sub_eq_zero_of_eq IsPrimitiveRoot.arg_eq_pi_iff Complex.arg_eq_pi_iff IsPrimitiveRoot.neg_one CharP.ofCharZero Complex.instCharZero two_ne_zero abs_eq_self norm_neg norm_add_lt_of_not_sameRay UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace cyclotomic.eval_apply_ofReal LT.lt.ne cyclotomic_pos' Complex.nnnorm_real lt_of_not_ge Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_neg_of_lt cyclotomic_eq_prod_X_sub_primitiveRoots eval_prod Finset.prod_congr eval_sub eval_X eval_C nnnorm_prod NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Finset.prod_eq_zero add_pos' lt_trans Mathlib.Meta.Positivity.pos_of_isNat Finset.prod_const Finset.card_attach Complex.card_primitiveRoots Finset.prod_lt_prod' IsOrderedMonoid.toIsOrderedCancelMonoid Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid Units.val_mk0 cyclotomic_nonneg max_eq_left_iff le_of_not_gt
cyclotomic_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing eval Ring.toSemiring cyclotomic	—	cyclotomic_pos_and_nonneg
cyclotomic_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing eval Ring.toSemiring CommRing.toRing cyclotomic	—	Nat.strong_induction_on pos_of_gt Nat.instCanonicallyOrderedAdd LT.lt.trans Nat.instAtLeastTwoHAddOfNat one_lt_two Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid prod_cyclotomic_eq_geom_sum lt_trichotomy pos_of_mul_pos_left MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono eval_geom_sum eval_mul Nat.self_notMem_properDivisors Finset.erase_subset Finset.prod_cons Finset.erase_cons_of_ne LT.lt.ne' Nat.cons_self_properDivisors eval_prod Finset.prod_nonneg IsStrictOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing geom_sum_pos_iff LT.lt.le Nat.two_lt_of_ne zero_dvd_iff Nat.not_odd_iff_even even_iff_two_dvd eq_or_ne cyclotomic_two eval_add eval_X eval_one geom_sum_eq_zero_iff_neg_one pos_of_mul_neg_left AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add IsOrderedRing.toIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Finset.mem_erase Nat.mem_properDivisors geom_sum_neg_iff Finset.prod_erase_mul mul_nonpos_of_nonneg_of_nonpos le_of_lt
cyclotomic_pos' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing eval Ring.toSemiring cyclotomic	—	cyclotomic_pos_and_nonneg
cyclotomic_pos_and_nonneg 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing eval Ring.toSemiring CommRing.toRing cyclotomic Preorder.toLE	—	cyclotomic_zero eval_one IsStrictOrderedRing.toZeroLEOneClass NeZero.one instNontrivialOfCharZero IsStrictOrderedRing.toCharZero zero_add cyclotomic_one eval_sub eval_X IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing cyclotomic_two eval_add 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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_congr 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.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 Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le le_of_not_gt cyclotomic_pos le_of_lt
eval_one_cyclotomic_not_prime_pow 📖	mathematical	—	eval Ring.toSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne cyclotomic	—	cyclotomic_zero eval_one LT.lt.ne' Nat.prime_two Nat.eq_one_iff_not_exists_prime_dvd prod_cyclotomic_eq_geom_sum mul_assoc mul_comm mul_left_comm Finset.prod_singleton Finset.prod_sdiff Finset.card_range Finset.prod_const Finset.prod_congr eval_one_cyclotomic_prime_pow Finset.prod_image Nat.succ_injective Nat.pow_right_injective Nat.Prime.two_le range_pow_padicValNat_subset_divisors' eval_prod one_geom_sum eval_geom_sum pow_succ_padicValNat_not_dvd eval_intCast_map Int.cast_one map_cyclotomic eq_intCast RingHom.instRingHomClass 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.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add 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 Mathlib.Tactic.Linarith.lt_of_lt_of_eq neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing cyclotomic_nonneg le_refl
eval_one_cyclotomic_prime 📖	mathematical	—	eval Ring.toSemiring CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne cyclotomic AddMonoidWithOne.toNatCast	—	cyclotomic_prime eval_finset_sum Finset.sum_congr eval_pow eval_X one_pow Finset.sum_const Finset.card_range Nat.smul_one_eq_cast
eval_one_cyclotomic_prime_pow 📖	mathematical	—	eval Ring.toSemiring CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne cyclotomic Monoid.toNatPow Nat.instMonoid AddMonoidWithOne.toNatCast	—	cyclotomic_prime_pow_eq_geom_sum Fact.out eval_finset_sum Finset.sum_congr eval_pow eval_X one_pow Finset.sum_const Finset.card_range Nat.smul_one_eq_cast
eval₂_one_cyclotomic_prime 📖	mathematical	—	eval₂ CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring cyclotomic CommRing.toRing AddMonoidWithOne.toNatCast	—	eval₂_at_one eval_one_cyclotomic_prime map_natCast RingHom.instRingHomClass
eval₂_one_cyclotomic_prime_pow 📖	mathematical	—	eval₂ CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring cyclotomic Monoid.toNatPow Nat.instMonoid CommRing.toRing AddMonoidWithOne.toNatCast	—	eval₂_at_one eval_one_cyclotomic_prime_pow map_natCast RingHom.instRingHomClass
sub_one_lt_natAbs_cyclotomic_eval 📖	mathematical	—	eval Ring.toSemiring Int.instRing cyclotomic	—	LT.lt.ne' Nat.totient_pos pos_of_gt Nat.instCanonicallyOrderedAdd sub_one_pow_totient_lt_natAbs_cyclotomic_eval
sub_one_pow_totient_le_cyclotomic_eval 📖	mathematical	Real Real.instLT Real.instOne	Real.instLE Monoid.toNatPow Real.instMonoid Real.instSub Nat.totient eval Ring.toSemiring Real.instRing cyclotomic	—	pow_zero cyclotomic_zero eval_one pow_one cyclotomic_one eval_sub eval_X LT.lt.le sub_one_pow_totient_lt_cyclotomic_eval le_add_self Nat.instCanonicallyOrderedAdd
sub_one_pow_totient_lt_cyclotomic_eval 📖	mathematical	Real Real.instLT Real.instOne	Monoid.toNatPow Real.instMonoid Real.instSub Nat.totient eval Ring.toSemiring Real.instRing cyclotomic	—	pos_of_gt Nat.instCanonicallyOrderedAdd LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.one Real.instNontrivial instIsDomain Complex.norm_real Real.norm_of_nonneg LT.lt.le IsPrimitiveRoot.norm'_eq_one mem_primitiveRoots LT.lt.ne' norm_sub_norm_le Nat.instAtLeastTwoHAddOfNat Complex.isPrimitiveRoot_exp Real.instIsStrictOrderedRing Complex.sameRay_iff Nat.cast_zero IsPrimitiveRoot.ne_zero Complex.instNontrivial Complex.arg_ofReal_of_nonneg IsPrimitiveRoot.arg_eq_zero_iff 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.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 Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq 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 sub_eq_zero_of_eq Nat.cast_one IsPrimitiveRoot.unique IsPrimitiveRoot.one lt_norm_sub_of_not_sameRay UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace cyclotomic.eval_apply_ofReal cyclotomic_pos' AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add Complex.nnnorm_real cyclotomic_eq_prod_X_sub_primitiveRoots eval_prod Finset.prod_congr eval_sub eval_X eval_C nnnorm_prod NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Finset.prod_eq_zero Finset.prod_const Finset.card_attach Complex.card_primitiveRoots Finset.prod_lt_prod' IsOrderedMonoid.toIsOrderedCancelMonoid Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid Units.val_mk0 sup_of_le_left cyclotomic_nonneg
sub_one_pow_totient_lt_natAbs_cyclotomic_eval 📖	mathematical	—	Monoid.toNatPow Nat.instMonoid Nat.totient eval Ring.toSemiring Int.instRing cyclotomic	—	Ne.lt_or_gt zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub zero_pow LT.lt.ne' Nat.totient_pos pos_of_gt pos_iff_ne_zero Nat.cast_zero coeff_zero_eq_eval_zero cyclotomic_coeff_zero one_ne_zero Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Nat.cast_pow Nat.cast_sub LT.lt.le Nat.cast_one Nat.cast_natAbs LT.lt.trans_le sub_one_pow_totient_lt_cyclotomic_eval Nat.one_lt_cast Int.cast_abs Real.instIsStrictOrderedRing eq_intCast RingHom.instRingHomClass Eq.trans_le cyclotomic.eval_apply le_abs_self

---

← Back to Index