Approximation

📁 Source: Mathlib/Analysis/Normed/Field/Approximation.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_aroots_norm_sub_lt_of_norm_coeff_sub_lt, exists_monic_and_natDegree_eq_and_norm_map_algebraMap_coeff_sub_lt, exists_roots_norm_sub_lt_of_norm_coeff_sub_lt	3
Total	3

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_aroots_norm_sub_lt_of_norm_coeff_sub_lt 📖	mathematical	Real Real.instLT Real.instZero DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring algebraOfAlgebra Algebra.id NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AlgHom.funLike aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Monic natDegree Norm.norm NormedField.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing coeff Splits map algebraMap	Multiset Multiset.instMembership aroots EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField instIsDomain Field.toSemifield NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Real Real.instLT Norm.norm NormedField.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Real.instMul Real.instPow Real.instAdd Real.instNatCast natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Real.instOne Real.instInv Real.instMax	—	instIsDomain exists_roots_norm_sub_lt_of_norm_coeff_sub_lt eval_map_algebraMap Monic.map natDegree_map DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing coeff_map RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass norm_algebraMap' NormedDivisionRing.to_normOneClass
exists_monic_and_natDegree_eq_and_norm_map_algebraMap_coeff_sub_lt 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring NormedField.toField RingHom.instFunLike algebraMap Monic Real Real.instLT Real.instZero	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Monic natDegree NormedField.toField Real Real.instLT Norm.norm NormedField.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing coeff map algebraMap Semifield.toCommSemiring	—	Monic.natDegree_eq_zero natDegree_one map_one sub_self norm_zero natDegree_add_eq_left_of_natDegree_lt map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_mul natDegree_pow IsDomain.to_noZeroDivisors instIsDomain natDegree_X IsLocalRing.toNontrivial Field.instIsLocalRing mul_one natDegree_sum_le_of_forall_le LE.le.trans natDegree_C_mul_X_pow_le Monic.eq_1 leadingCoeff.eq_1 coeff_add coeff_X_pow finset_sum_coeff Finset.sum_congr coeff_C_mul mul_ite MulZeroClass.mul_zero Finset.sum_ite_eq add_zero lt_trichotomy map_add map_pow map_X ne_of_lt coeff_map zero_add map_zero MonoidWithZeroHomClass.toZeroHomClass Monic.leadingCoeff ne_of_gt not_lt_of_gt coeff_eq_zero_of_natDegree_lt Metric.denseRange_iff
exists_roots_norm_sub_lt_of_norm_coeff_sub_lt 📖	mathematical	Real Real.instLT Real.instZero eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Monic natDegree Norm.norm NormedField.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing coeff Splits	Multiset Multiset.instMembership roots EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField instIsDomain Field.toSemifield Real Real.instLT Norm.norm NormedField.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Real.instMul Real.instPow Real.instAdd Real.instNatCast natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Real.instOne Real.instInv Real.instMax	—	instIsDomain Multiset.prod_hom' MonoidWithZeroHomClass.toMonoidHomClass MulRingSeminormClass.toMonoidWithZeroHomClass MulRingNormClass.toMulRingSeminormClass MulRingNorm.mulRingNormClass Splits.eval_eq_prod_roots_of_monic sub_add_cancel norm_add_le eval_sub norm_zero add_zero as_sum_range' Nat.instNoMaxOrder max_self natDegree_sub_le coeff_sub map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass norm_sum_le Finset.sum_congr eval_finset_sum eval_mul eval_C eval_pow eval_X norm_mul NormedDivisionRing.toNormMulClass norm_pow NormedDivisionRing.to_normOneClass Real.rpow_natCast mul_assoc Finset.sum_const Finset.card_range nsmul_eq_mul Nat.cast_add Nat.cast_one Finset.sum_lt_sum_of_nonempty Real.instIsOrderedCancelAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.nonempty_range_add_one mul_lt_mul_of_lt_of_le_of_nonneg_of_pos IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing LE.le.trans pow_le_pow_left₀ IsOrderedRing.toMulPosMono norm_nonneg le_max_left pow_le_pow_right₀ Real.instZeroLEOneClass le_max_right pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass lt_max_of_lt_right Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Multiset.prod_map_le_prod_map₀ le_of_lt mul_pos Real.rpow_pos_of_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.cast_nonneg' Mathlib.Tactic.Push.not_and_eq Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr 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.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.rpow_one inv_mul_cancel₀ RCLike.charZero_rclike eval_one NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing Multiset.map_const' Splits.natDegree_eq_card_roots Multiset.prod_replicate mul_pow Real.rpow_mul LT.lt.le

---

← Back to Index