RootsExtrema

📁 Source: Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_eval_T_real_eq_one_iff, abs_eval_T_real_le_one, abs_eval_T_real_le_one_iff, eval_T_real_cos_int_mul_pi_div, eval_T_real_eq_neg_one_iff, eval_T_real_eq_one_iff, eval_T_real_mem_Icc, irrational_of_isRoot_T_real, isExtrOn_T_real, isExtrOn_T_real_iff, isLocalExtr_T_real, isLocalExtr_T_real_iff, isLocalMax_T_real, isLocalMin_T_real, isMaxOn_T_real, isMinOn_T_real, one_le_abs_eval_T_real, one_le_eval_T_real, one_le_negOnePow_mul_eval_T_real, one_lt_abs_eval_T_real, one_lt_eval_T_real, one_lt_negOnePow_mul_eval_T_real, rootMultiplicity_T_real, rootMultiplicity_U_real, roots_T_real, roots_T_real_nodup, roots_U_real, roots_U_real_nodup	28
Total	28

Polynomial.Chebyshev

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_eval_T_real_eq_one_iff 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.instOne Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	abs_eval_T_real_le_one_iff Nat.cast_ne_zero Int.instCharZero le_of_eq Real.abs_cos_eq_one_iff Int.cast_natCast T_real_cos Real.cos_arccos neg_le_of_abs_le Real.instIsOrderedAddMonoid le_of_max_le_left Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Real.pi_pos Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial CanLift.prf instCanLiftIntNatCastLeOfNat Int.cast_nonneg_iff IsOrderedAddMonoid.toAddLeftMono Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.arccos_nonneg mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt Nat.cast_pos' lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_le_mul_of_nonneg_left div_le_one_of_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.arccos_le_pi mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero
abs_eval_T_real_le_one 📖	mathematical	Real Real.instLE abs Real.lattice Real.instAddGroup Real.instOne	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T	—	—
abs_eval_T_real_le_one_iff 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup Real.instOne Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T	—	abs_eval_T_real_le_one one_lt_abs_eval_T_real
eval_T_real_cos_int_mul_pi_div 📖	mathematical	—	Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi T Real.instIntCast Units.val Int.instMonoid Int.negOnePow	—	T_real_cos Int.cast_negOnePow Int.cast_natCast Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Real.pi_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial Real.cos_int_mul_pi
eval_T_real_eq_neg_one_iff 📖	mathematical	—	Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.instNeg Real.instOne Odd Nat.instSemiring Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	abs_eval_T_real_eq_one_iff abs_eq_abs abs_neg abs_one Real.instIsOrderedRing neg_one_pow_eq_neg_one_iff_odd Int.cast_negOnePow_natCast eval_T_real_cos_int_mul_pi_div Int.negOnePow_odd Int.odd_coe_nat Nat.cast_one RCLike.charZero_rclike
eval_T_real_eq_one_iff 📖	mathematical	—	Polynomial.eval Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.instOne Even Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	abs_eval_T_real_eq_one_iff abs_eq_abs abs_one Real.instIsOrderedRing neg_one_pow_eq_one_iff_even Int.cast_negOnePow_natCast eval_T_real_cos_int_mul_pi_div Int.negOnePow_even Int.even_coe_nat Nat.cast_one Int.cast_one RCLike.charZero_rclike
eval_T_real_mem_Icc 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instNeg Real.instOne	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T	—	Real.cos_arccos
irrational_of_isRoot_T_real 📖	mathematical	Polynomial.IsRoot Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T	Irrational	—	Nat.instAtLeastTwoHAddOfNat Finset.mem_image Real.instIsDomain roots_T_real Polynomial.mem_roots T_ne_zero ZeroLEOneClass.neZero.two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid irrational_cos_rat_mul_pi Mathlib.Tactic.Contrapose.contrapose₂ Nat.cast_zero Nat.cast_one Int.instCharZero IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.instCharZero Nat.cast_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ one_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Nat.cast_pos' lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.pi_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial Real.cos_pi_div_two Rat.cast_divInt Int.cast_add Int.cast_mul Int.cast_ofNat Int.cast_natCast Int.cast_one Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Nat.cast_nonneg'
isExtrOn_T_real 📖	mathematical	—	IsExtrOn Real Real.instPreorder Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Set.Icc Real.instNeg Real.instOne Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	Nat.even_or_odd isMaxOn_T_real isMinOn_T_real
isExtrOn_T_real_iff 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instNeg Real.instOne	IsExtrOn Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	abs_eval_T_real_eq_one_iff eq_of_le_of_ge abs_eval_T_real_le_one IsExtrOn.elim le_abs le_neg_of_le_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add isMinOn_iff eval_T_real_eq_neg_one_iff one_mul Nat.cast_one isMaxOn_iff MulZeroClass.zero_mul zero_div Real.cos_zero Real.instZeroLEOneClass eval_T_real_eq_one_iff Nat.instCanonicallyOrderedAdd CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike isExtrOn_T_real
isLocalExtr_T_real 📖	mathematical	—	IsLocalExtr Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	Nat.even_or_odd isLocalMax_T_real isLocalMin_T_real
isLocalExtr_T_real_iff 📖	mathematical	—	IsLocalExtr Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Finset Finset.instMembership Finset.Ioo Nat.instPreorder Nat.instLocallyFiniteOrder Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	IsLocalExtr.deriv_eq_zero Real.instIsDomain Polynomial.mem_roots Polynomial.degree_ne_bot ne_of_eq_of_ne WithBot.natCast_ne_bot mul_eq_zero_iff_left NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike Nat.instCanonicallyOrderedAdd Nat.instCharZero Nat.instAtLeastTwoHAddOfNat Polynomial.eval_natCast Int.cast_natCast Polynomial.eval_mul T_derivative_eq_U Polynomial.deriv Finset.mem_image roots_U_real Finset.mem_Ioo Nat.cast_one isLocalExtr_T_real
isLocalMax_T_real 📖	mathematical	Even	IsLocalMax Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.pi_pos lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd div_lt_div_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono mul_lt_mul_of_pos_right Nat.strictMono_cast mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Nat.cast_ne_zero eventually_nhds_iff eval_T_real_eq_one_iff le_of_lt abs_le abs_eval_T_real_le_one isOpen_Ioo HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.cos_pi Real.cos_lt_cos_of_nonneg_of_le_pi le_refl Real.cos_zero
isLocalMin_T_real 📖	mathematical	Odd Nat.instSemiring	IsLocalMin Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	Odd.pos Nat.instCanonicallyOrderedAdd Nat.instNontrivial div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.pi_pos lt_of_le_of_ne' zero_le div_lt_div_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono mul_lt_mul_of_pos_right Nat.strictMono_cast mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Nat.cast_ne_zero eventually_nhds_iff eval_T_real_eq_neg_one_iff le_of_lt abs_le abs_eval_T_real_le_one isOpen_Ioo HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.cos_pi Real.cos_lt_cos_of_nonneg_of_le_pi le_refl Real.cos_zero
isMaxOn_T_real 📖	mathematical	Even	IsMaxOn Real Real.instPreorder Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Set.Icc Real.instNeg Real.instOne Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	isMaxOn_iff abs_le Real.instIsOrderedAddMonoid abs_eval_T_real_le_one eval_T_real_eq_one_iff
isMinOn_T_real 📖	mathematical	Odd Nat.instSemiring	IsMinOn Real Real.instPreorder Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Set.Icc Real.instNeg Real.instOne Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNatCast Real.pi	—	isMinOn_iff eval_T_real_eq_neg_one_iff abs_le Real.instIsOrderedAddMonoid abs_eval_T_real_le_one
one_le_abs_eval_T_real 📖	mathematical	Real Real.instLE Real.instOne abs Real.lattice Real.instAddGroup	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T	—	LE.le.trans one_le_eval_T_real abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_abs_self T_eval_neg abs_mul Real.instIsOrderedRing abs_unit_intCast one_mul
one_le_eval_T_real 📖	mathematical	Real Real.instLE Real.instOne	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T	—	Real.cosh_arcosh
one_le_negOnePow_mul_eval_T_real 📖	mathematical	Real Real.instLE Real.instNeg Real.instOne	Real.instMul Real.instIntCast Units.val Int.instMonoid Int.negOnePow Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T	—	neg_neg T_eval_neg Int.cast_negOnePow mul_assoc mul_zpow mul_neg mul_one one_zpow one_mul one_le_eval_T_real le_neg_of_le_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
one_lt_abs_eval_T_real 📖	mathematical	Real Real.instLT Real.instOne abs Real.lattice Real.instAddGroup	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T	—	LT.lt.trans_le one_lt_eval_T_real abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_abs_self T_eval_neg abs_mul Real.instIsOrderedRing abs_unit_intCast one_mul
one_lt_eval_T_real 📖	mathematical	Real Real.instLT Real.instOne	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T	—	Real.cosh_arcosh le_of_lt T_real_cosh Real.one_lt_cosh mul_ne_zero_iff NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.cast_zero Int.cast_zero RCLike.charZero_rclike
one_lt_negOnePow_mul_eval_T_real 📖	mathematical	Real Real.instLT Real.instNeg Real.instOne	Real.instMul Real.instIntCast Units.val Int.instMonoid Int.negOnePow Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T	—	neg_neg T_eval_neg Int.cast_negOnePow mul_assoc mul_zpow mul_neg mul_one one_zpow one_mul one_lt_eval_T_real lt_neg_of_lt_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add
rootMultiplicity_T_real 📖	mathematical	—	Polynomial.rootMultiplicity Real Real.instRing Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instOne Real.pi T Real.commRing	—	Nat.instAtLeastTwoHAddOfNat Real.instIsDomain Polynomial.count_roots roots_T_real Multiset.count_eq_one_of_mem
rootMultiplicity_U_real 📖	mathematical	—	Polynomial.rootMultiplicity Real Real.instRing Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instAdd Real.instNatCast Real.instOne Real.pi U Real.commRing	—	Real.instIsDomain Polynomial.count_roots roots_U_real Multiset.count_eq_one_of_mem
roots_T_real 📖	mathematical	—	Polynomial.roots Real Real.commRing Real.instIsDomain T Finset.val Finset.image Real.decidableEq Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instOne Real.pi Finset.range	—	Real.instIsDomain Nat.instAtLeastTwoHAddOfNat Polynomial.roots_eq_of_degree_eq_card Finset.mem_image T_real_cos Real.cos_eq_zero_iff Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Real.pi_pos Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Nat.cast_one Nat.cast_add Nat.cast_mul Int.cast_add Int.cast_mul Int.cast_ofNat Int.cast_natCast Int.cast_one Int.instCharZero Finset.card_image_of_injOn Finset.nodup_map_iff_injOn roots_T_real_nodup Finset.card_range degree_T ZeroLEOneClass.neZero.two Polynomial.roots.congr_simp CharP.cast_eq_zero CharP.ofCharZero T_zero Polynomial.roots_one MulZeroClass.mul_zero div_zero Real.cos_zero
roots_T_real_nodup 📖	mathematical	—	Multiset.Nodup Real Multiset.map Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instOne Real.pi Multiset.range	—	Nat.instAtLeastTwoHAddOfNat Finset.nodup_map_iff_injOn Set.InjOn.comp Real.injOn_cos Finset.coe_range NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain AddRightCancelSemigroup.toIsRightCancelAdd IsCancelMulZero.toIsLeftCancelMulZero Set.mem_Icc le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_nonneg' Real.instZeroLEOneClass Nat.cast_one Real.pi_pos Nat.cast_pos' NeZero.charZero_one lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Tactic.FieldSimp.NF.cons_pos zero_lt_one NeZero.one GroupWithZero.toNontrivial Multiset.map_congr CharP.cast_eq_zero CharP.ofCharZero MulZeroClass.mul_zero div_zero Real.cos_zero
roots_U_real 📖	mathematical	—	Polynomial.roots Real Real.commRing Real.instIsDomain U Finset.val Finset.image Real.decidableEq Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instAdd Real.instNatCast Real.instOne Real.pi Finset.range	—	Real.instIsDomain Polynomial.roots_eq_of_degree_eq_card Finset.mem_image U_real_cos Real.sin_eq_zero_iff Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_pos' Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Real.pi_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial Nat.cast_add Int.cast_add Int.cast_natCast Int.cast_one Nat.cast_mul Int.instCharZero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul mul_eq_zero_iff_right NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.sin_pos_of_pos_of_lt_pi div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.cast_nonneg' Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt LT.lt.ne' Mathlib.Tactic.FieldSimp.NF.cons_pos zero_lt_one Finset.card_image_of_injOn Finset.nodup_map_iff_injOn roots_U_real_nodup Finset.card_range degree_U_natCast ZeroLEOneClass.neZero.two Polynomial.roots.congr_simp CharP.cast_eq_zero CharP.ofCharZero U_zero Polynomial.roots_one zero_add
roots_U_real_nodup 📖	mathematical	—	Multiset.Nodup Real Multiset.map Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instAdd Real.instNatCast Real.instOne Real.pi Multiset.range	—	Finset.nodup_map_iff_injOn Set.InjOn.comp Real.injOn_cos AddRightCancelSemigroup.toIsRightCancelAdd RCLike.charZero_rclike Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_nonneg' Real.instZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Real.pi_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial Set.mem_Icc le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Tactic.FieldSimp.NF.cons_pos zero_lt_one

---

← Back to Index