Hensel

📁 Source: Mathlib/NumberTheory/Padics/Hensel.lean

Statistics

Metric	Count
Definitions	0
Theorems hensels_lemma, limit_zero_of_norm_tendsto_zero, padic_polynomial_dist	3
Total	3

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hensels_lemma 📖	mathematical	Real Real.instLT Norm.norm PadicInt PadicInt.instNorm DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring CommRing.toCommSemiring PadicInt.instCommRing Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval Monoid.toNatPow Real.instMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing PadicInt.instNormedCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing	—	—
limit_zero_of_norm_tendsto_zero 📖	mathematical	Filter.Tendsto Real Norm.norm PadicInt PadicInt.instNorm DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring CommRing.toCommSemiring PadicInt.instCommRing Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval IsCauSeq Real.instField Real.linearOrder Real.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing PadicInt.instNormedCommRing Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	CauSeq.lim NormMulClass.isAbsoluteValue_norm PadicInt.instNormMulClass PadicInt.complete MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	—	Real.instIsStrictOrderedRing tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace NormMulClass.isAbsoluteValue_norm PadicInt.instNormMulClass PadicInt.complete Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Polynomial.eval_map_algebraMap Filter.Tendsto.congr
padic_polynomial_dist 📖	mathematical	—	Real Real.instLE Norm.norm PadicInt PadicInt.instNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing PadicInt.instNormedCommRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring CommRing.toCommSemiring PadicInt.instCommRing Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	Polynomial.eval_map_algebraMap norm_mul PadicInt.instNormMulClass mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing PadicInt.norm_le_one norm_nonneg one_mul

---

← Back to Index