Dense

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

Statistics

Metric	Count
Definitions	0
Theorems of_denseRange	1
Total	1

IsAlgClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_denseRange 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring NormedField.toField RingHom.instFunLike algebraMap	IsAlgClosed NormedField.toField NontriviallyNormedField.toNormedField	—	of_exists_root LT.lt.ne' Irreducible.natDegree_pos Polynomial.SplittingField.splits Polynomial.degree_map DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing CharP.cast_eq_zero CharP.ofCharZero WithBot.charZero Nat.instCharZero Polynomial.degree_ne_of_natDegree_ne Algebra.IsSeparable.isAlgebraic Algebra.IsSeparable.of_integral instIsDomain Algebra.IsIntegral.of_finite Polynomial.IsSplittingField.instFiniteDimensionalSplittingField Polynomial.eval_map_algebraMap Polynomial.eval_rootOfSplits Finset.image_nonempty Finset.min'_le Finset.mem_image_of_mem Finset.filter.congr_simp Set.toFinset_congr minpoly.eq_of_irreducible_of_monic isConjRoot_iff_mem_minpoly_rootSet norm_pos_iff sub_ne_zero lt_of_not_ge 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 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.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono pow_pos IsStrictOrderedRing.toZeroLEOneClass lt_max_of_lt_right Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial add_pos' IsOrderedAddMonoid.toAddLeftMono Nat.cast_pos' Real.instZeroLEOneClass NeZero.one lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Polynomial.exists_monic_and_natDegree_eq_and_norm_map_algebraMap_coeff_sub_lt Polynomial.exists_aroots_norm_sub_lt_of_norm_coeff_sub_lt Polynomial.Monic.map Polynomial.natDegree_map Polynomial.map_map Polynomial.Splits.map splits Real.rpow_one div_mul_cancel₀ mul_inv_cancel₀ RCLike.charZero_rclike Real.rpow_mul LT.lt.le one_mul div_self ne_of_gt mul_comm_div Real.rpow_natCast Multiset.mem_map Polynomial.Splits.roots_map Polynomial.aroots_def IntermediateField.mem_bot IntermediateField.adjoin_simple_eq_bot_iff IsKrasner.krasner IsKrasner.of_completeSpace Algebra.IsAlgebraic.isSeparable_of_perfectField PerfectField.ofCharZero Irreducible.separable minpoly.irreducible lt_of_lt_of_le RingHom.injective Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

---

← Back to Index