PadicNumbers

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

Statistics

Metric	Count
Definitions padicValuation, addValuation, addValuationDef, instAdd, instAddCommGroup, instCommRing, instDist, instDiv, instInhabited, instMul, instNeg, instNontriviallyNormedField, instNorm, instOne, instRing, instSub, instZero, limSeq, metricSpace, mk, mulValuation, normedField, ratNorm, valuation, PadicSeq, norm, stationaryPoint, valuation, padicValuation, padicNormE, «termℚ_[_]»	31
Theorems padicValuation_eq_one_iff, padicValuation_eq_zero_iff, padicValuation_le_one, padicValuation_lt_one_iff, padicValuation_self, map_add, map_mul, map_one, map_zero, apply, add_eq_max_of_ne, coe_add, coe_div, coe_inj, coe_mul, coe_neg, coe_one, coe_sub, coe_zero, comap_mulValuation_eq_int_padicValuation, comap_mulValuation_eq_padicValuation, complete, complete', complete'', const_equiv, denseRange_ratCast, eq_of_norm_add_lt_left, eq_of_norm_add_lt_right, eq_padicNorm, eq_ratNorm, exi_rat_seq_conv, exi_rat_seq_conv_cauchy, instCharZero, instCompleteSpace, instIsUltrametricDist, isAbsoluteValue, le_valuation_add, mk_eq, mulValuation_toFun, nonarchimedean, norm_eq_of_norm_add_lt_left, norm_eq_of_norm_add_lt_right, norm_eq_of_norm_sub_lt_left, norm_eq_of_norm_sub_lt_right, norm_eq_zpow_log_mulValuation, norm_eq_zpow_neg_valuation, norm_intCast_eq_one_iff, norm_intCast_lt_one_iff, norm_int_le_one, norm_int_le_pow_iff_dvd, norm_le_one_iff_val_nonneg, norm_le_pow_iff_norm_lt_pow_add_one, norm_lt_pow_iff_norm_le_pow_sub_one, norm_natCast_eq_one_iff, norm_natCast_lt_one_iff, norm_natCast_p_sub_one, norm_p, norm_p_lt_one, norm_p_pow, norm_p_zpow, norm_rat_le_one, image, is_norm, is_rat, mul, padicNormE_lim_le, rat_dense, rat_dense', valuation_intCast, valuation_inv, valuation_mul, valuation_natCast, valuation_ofNat, valuation_one, valuation_p, valuation_pow, valuation_ratCast, valuation_zero, valuation_zpow, zero_def, add_eq_max_of_ne, eq_zero_iff_equiv_zero, equiv_zero_of_val_eq_of_equiv_zero, lift_index_left, lift_index_left_left, lift_index_right, ne_zero_iff_nequiv_zero, norm_const, norm_eq, norm_eq_norm_app_of_nonzero, norm_eq_of_add_equiv_zero, norm_eq_zpow_neg_valuation, norm_equiv, norm_mul, norm_neg, norm_nonarchimedean, norm_nonneg, norm_nonzero_of_not_equiv_zero, norm_one, norm_values_discrete, norm_zero_iff, not_equiv_zero_const_of_nonzero, not_limZero_const_of_nonzero, stationary, stationaryPoint_spec, val_eq_iff_norm_eq, padicValuation_cast, padicValuation_eq_zero_iff, padicValuation_le_one_iff, padicValuation_self, surjective_padicValuation, add_eq_max_of_ne', defn, eq_padic_norm', image', nonarchimedean'	116
Total	147

Int

Definitions

Name	Category	Theorems
padicValuation 📖	CompOp	7 math math: Rat.padicValuation_cast, padicValuation_lt_one_iff, padicValuation_eq_one_iff, padicValuation_self, Padic.comap_mulValuation_eq_int_padicValuation, padicValuation_le_one, padicValuation_eq_zero_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
padicValuation_eq_one_iff 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid instAddCommMonoid Multiplicative.linearOrder instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid instSemiring instIsStrictOrderedRing instRing Valuation.instFunLike padicValuation WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid instIsStrictOrderedRing padicValRat.of_int NeZero.one WithZero.instNontrivial WithZero.exp_zero WithZero.exp_injective Nat.Prime.ne_one Fact.out
padicValuation_eq_zero_iff 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid instAddCommMonoid Multiplicative.linearOrder instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid instSemiring instIsStrictOrderedRing instRing Valuation.instFunLike padicValuation WithZero.instZero	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid instIsStrictOrderedRing WithZero.instNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Rat.instCharZero
padicValuation_le_one 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid instAddCommMonoid Multiplicative.linearOrder instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid instSemiring instIsStrictOrderedRing instRing Valuation.instFunLike padicValuation WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid instIsStrictOrderedRing padicValRat.of_int WithZero.le_log_iff_exp_le NeZero.one WithZero.instNontrivial instAddLeftMono IsStrictOrderedRing.toIsOrderedRing
padicValuation_lt_one_iff 📖	mathematical	—	WithZero Multiplicative Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid instAddCommMonoid Multiplicative.linearOrder instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid instSemiring instIsStrictOrderedRing instRing Valuation.instFunLike padicValuation WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid instIsStrictOrderedRing
padicValuation_self 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid instAddCommMonoid Multiplicative.linearOrder instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid instSemiring instIsStrictOrderedRing instRing Valuation.instFunLike padicValuation WithZero.exp	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid instIsStrictOrderedRing cast_natCast Rat.padicValuation_self

Padic

Definitions

Name	Category	Theorems
addValuation 📖	CompOp	1 math math: addValuation.apply
addValuationDef 📖	CompOp	4 math math: AddValuation.map_one, AddValuation.map_add, AddValuation.map_zero, AddValuation.map_mul
instAdd 📖	CompOp	11 math math: padicNormE.nonarchimedean', padicNormE.add_eq_max_of_ne', AddValuation.map_add, le_valuation_add, toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, nonarchimedean, coe_withValRingEquiv, coe_withValRingEquiv_symm, coe_add, add_eq_max_of_ne, PadicInt.coe_add
instAddCommGroup 📖	CompOp	—
instCommRing 📖	CompOp	5 math math: instCompatibleWithZeroMultiplicativeIntMulValuation, PadicAlgCl.isAlgebraic, instIsRankLeOne, instIsNontrivial, comap_mulValuation_eq_int_padicValuation
instDist 📖	CompOp	1 math math: instIsUltrametricDist
instDiv 📖	CompOp	1 math math: coe_div
instInhabited 📖	CompOp	—
instMul 📖	CompOp	10 math math: coe_mul, valuation_mul, toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, padicNormE.mul, coe_withValRingEquiv, AddValuation.map_mul, coe_withValRingEquiv_symm, PadicInt.coe_mul, PadicInt.unitCoeff_coe, PadicInt.coe_dpow_eq
instNeg 📖	CompOp	2 math math: coe_neg, PadicInt.coe_neg
instNontriviallyNormedField 📖	CompOp	—
instNorm 📖	CompOp	58 math math: eq_ratNorm, PadicInt.coe_sub, PadicInt.norm_intCast_eq_padic_norm, PadicInt.mem_subring_iff, PadicInt.coe_zero, norm_intCast_eq_one_iff, eq_padicNorm, withValUniformEquiv_norm_le_one_iff, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, PadicInt.coe_eq_zero, PadicInt.padic_norm_e_of_padicInt, PadicInt.coe_sum, norm_int_le_one, PadicInt.algebraMap_apply, norm_eq_zpow_log_mulValuation, PadicAlgCl.norm_extends, PadicInt.mk_coe, norm_natCast_lt_one_iff, norm_p_pow, norm_p_lt_one, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, PadicInt.coe_one, norm_eq_zpow_neg_valuation, PadicInt.coe_natCast, padicNormE.is_rat, PadicInt.valuation_coe_nonneg, padicNormE.is_norm, PadicInt.coe_adicCompletionIntegersEquiv_apply, norm_natCast_eq_one_iff, isAbsoluteValue, norm_le_one_iff_val_nonneg, norm_intCast_lt_one_iff, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, nonarchimedean, padicNormE.mul, PadicInt.valuation_coe, norm_rat_le_one, rat_dense, PadicInt.coe_neg, norm_rat_le_one_iff_padicValuation_le_one, PadicInt.norm_def, PadicInt.isOpenEmbedding_coe, norm_le_pow_iff_norm_lt_pow_add_one, add_eq_max_of_ne, norm_p, norm_natCast_p_sub_one, PadicInt.coe_mul, complete, PadicInt.coe_add, norm_lt_pow_iff_norm_le_pow_sub_one, PadicInt.unitCoeff_coe, PadicInt.coe_dpow_eq, PadicInt.coe_intCast, padicNormE.image, padicNorm_two_harmonic, norm_int_le_pow_iff_dvd, norm_p_zpow, PadicInt.coe_pow
instOne 📖	CompOp	4 math math: AddValuation.map_one, PadicInt.coe_one, valuation_one, coe_one
instRing 📖	CompOp	32 math math: PadicInt.norm_intCast_eq_padic_norm, PadicInt.mem_subring_iff, norm_intCast_eq_one_iff, complete', norm_int_le_one, addValuation.apply, instCharZero, norm_eq_zpow_log_mulValuation, valuation_p, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, norm_natCast_lt_one_iff, norm_p_pow, norm_p_lt_one, mulValuation_toFun, PadicInt.Coe.ringHom_apply, PadicInt.coe_natCast, norm_natCast_eq_one_iff, valuation_p_lt_one, complete'', exi_rat_seq_conv, valuation_intCast, norm_intCast_lt_one_iff, comap_mulValuation_eq_int_padicValuation, valuation_natCast, norm_p, norm_natCast_p_sub_one, complete, PadicInt.unitCoeff_coe, PadicInt.coe_dpow_eq, PadicInt.coe_intCast, norm_int_le_pow_iff_dvd, norm_p_zpow
instSub 📖	CompOp	8 math math: PadicInt.coe_sub, complete', coe_sub, padicNormE.defn, complete'', exi_rat_seq_conv, rat_dense, rat_dense'
instZero 📖	CompOp	8 math math: PadicInt.coe_zero, PadicInt.coe_eq_zero, coe_zero, zero_def, valuation_zero, mulValuation_toFun, AddValuation.map_zero, PadicInt.coe_dpow_eq
limSeq 📖	CompOp	2 math math: exi_rat_seq_conv_cauchy, exi_rat_seq_conv
metricSpace 📖	CompOp	—
mk 📖	CompOp	—
mulValuation 📖	CompOp	5 math math: instCompatibleWithZeroMultiplicativeIntMulValuation, norm_eq_zpow_log_mulValuation, mulValuation_toFun, comap_mulValuation_eq_padicValuation, comap_mulValuation_eq_int_padicValuation
normedField 📖	CompOp	30 math math: eq_padicNorm, withValUniformEquiv_norm_le_one_iff, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, PadicInt.coe_sum, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, instCompleteSpace, comap_mulValuation_eq_padicValuation, PadicAlgCl.instUniformContinuousConstSMulPadic, PadicAlgCl.spectralNorm_eq, PadicInt.coe_adicCompletionIntegersEquiv_apply, valuation_zpow, PadicComplex.instIsScalarTowerPadicPadicAlgCl, toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, denseRange_ratCast, valuation_ratCast, withValUniformEquiv_cast_apply, coe_withValRingEquiv, isUniformInducing_cast_withVal, norm_rat_le_one, rat_dense, coe_withValRingEquiv_symm, norm_rat_le_one_iff_padicValuation_le_one, PadicInt.isOpenEmbedding_coe, instProperSpace, PadicInt.unitCoeff_coe, padicNorm_two_harmonic, norm_p_zpow, isDenseInducing_cast_withVal
ratNorm 📖	CompOp	1 math math: eq_ratNorm
valuation 📖	CompOp	18 math math: addValuation.apply, valuation_p, valuation_zero, mulValuation_toFun, norm_eq_zpow_neg_valuation, valuation_mul, PadicInt.valuation_coe_nonneg, valuation_one, valuation_ofNat, valuation_zpow, le_valuation_add, valuation_intCast, norm_le_one_iff_val_nonneg, valuation_pow, PadicInt.valuation_coe, valuation_ratCast, valuation_natCast, valuation_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_max_of_ne 📖	mathematical	—	Norm.norm Padic instNorm instAdd Real Real.instMax	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing padicNormE.add_eq_max_of_ne'
coe_add 📖	mathematical	—	Padic DivisionRing.toRatCast Field.toDivisionRing field instAdd	—	Rat.cast_add instCharZero
coe_div 📖	mathematical	—	Padic DivisionRing.toRatCast Field.toDivisionRing field instDiv	—	Rat.cast_div instCharZero
coe_inj 📖	mathematical	—	Padic DivisionRing.toRatCast Field.toDivisionRing field	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat const_equiv Quotient.eq'
coe_mul 📖	mathematical	—	Padic DivisionRing.toRatCast Field.toDivisionRing field instMul	—	Rat.cast_mul instCharZero
coe_neg 📖	mathematical	—	Padic DivisionRing.toRatCast Field.toDivisionRing field instNeg	—	Rat.cast_neg
coe_one 📖	mathematical	—	Padic DivisionRing.toRatCast Field.toDivisionRing field instOne	—	—
coe_sub 📖	mathematical	—	Padic DivisionRing.toRatCast Field.toDivisionRing field instSub	—	Rat.cast_sub instCharZero
coe_zero 📖	mathematical	—	Padic DivisionRing.toRatCast Field.toDivisionRing field instZero	—	—
comap_mulValuation_eq_int_padicValuation 📖	mathematical	—	Valuation.comap Padic WithZero Multiplicative instRing WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing Int.instRing Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing instCommRing mulValuation Int.padicValuation	—	Valuation.ext Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing eq_intCast RingHom.instRingHomClass instCharZero valuation_intCast map_intCast
comap_mulValuation_eq_padicValuation 📖	mathematical	—	Valuation.comap Padic WithZero Multiplicative DivisionRing.toRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing normedField WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Rat.castHom instCharZero mulValuation Rat.padicValuation	—	Valuation.ext Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instCharZero eq_ratCast RingHom.instRingHomClass valuation_ratCast
complete 📖	mathematical	—	CauSeq.IsComplete Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing Padic instRing Norm.norm instNorm isAbsoluteValue	—	Real.instIsStrictOrderedRing isAbsoluteValue Rat.instIsStrictOrderedRing CauSeq.isCauSeq Nat.cast_zero complete'' exists_rat_btwn Real.instArchimedean lt_trans
complete' 📖	mathematical	—	DFunLike.coe AbsoluteValue Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field Rat.semiring Rat.instPartialOrder AbsoluteValue.funLike padicNormE instSub IsCauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing instRing	—	Rat.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat exi_rat_seq_conv half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono padicNormE.defn sub_add_sub_cancel LE.le.trans_lt AbsoluteValue.add_le add_halves CharZero.NeZero.two Rat.instCharZero add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Rat.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add le_of_max_le_right AbsoluteValue.map_sub IsStrictOrderedRing.toIsOrderedRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass le_of_max_le_left
complete'' 📖	mathematical	—	DFunLike.coe AbsoluteValue Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field Rat.semiring Rat.instPartialOrder AbsoluteValue.funLike padicNormE instSub IsCauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing instRing	—	Rat.instIsStrictOrderedRing complete' AbsoluteValue.map_sub IsStrictOrderedRing.toIsOrderedRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
const_equiv 📖	mathematical	—	CauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm CauSeq.equiv padicNorm.instIsAbsoluteValueRat CauSeq.const	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat eq_of_sub_eq_zero CauSeq.const_limZero
denseRange_ratCast 📖	mathematical	—	DenseRange Padic UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing normedField DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing	—	Metric.mem_closure_range_iff rat_dense
eq_of_norm_add_lt_left 📖	—	Real Real.instLT Norm.norm Padic instNorm instAdd	—	—	norm_eq_of_norm_add_lt_left
eq_of_norm_add_lt_right 📖	—	Real Real.instLT Norm.norm Padic instNorm instAdd	—	—	norm_eq_of_norm_add_lt_right
eq_padicNorm 📖	mathematical	—	Norm.norm Padic instNorm DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing normedField Real Real.instRatCast padicNorm	—	padicNormE.eq_padic_norm'
eq_ratNorm 📖	mathematical	—	Norm.norm Padic instNorm Real Real.instRatCast ratNorm	—	padicNormE.is_rat
exi_rat_seq_conv 📖	mathematical	—	DFunLike.coe AbsoluteValue Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field Rat.semiring Rat.instPartialOrder AbsoluteValue.funLike padicNormE instSub IsCauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing instRing DivisionRing.toRatCast Field.toDivisionRing limSeq	—	Rat.instIsStrictOrderedRing rat_dense' lt_of_lt_of_le div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_zero Nat.cast_one Rat.instAddLeftMono Rat.instZeroLEOneClass Rat.instCharZero right_distrib Distrib.rightDistribClass le_add_of_le_of_nonneg div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono le_trans le_of_lt one_mul exists_nat_gt instArchimedeanRat
exi_rat_seq_conv_cauchy 📖	mathematical	—	IsCauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm limSeq	—	Rat.instIsStrictOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.instAtLeastTwoHAddOfNat IsStrictOrderedRing.toIsOrderedRing Rat.nontrivial exi_rat_seq_conv CauSeq.cauchy₂ AbsoluteValue.isAbsoluteValue lt_of_le_of_lt AbsoluteValue.add_le add_thirds add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Rat.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add AbsoluteValue.map_sub NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass le_of_max_le_left le_of_max_le_right le_max_right sub_add_sub_cancel le_max_left padicNormE.eq_padic_norm' instCharZero Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg add_zero Mathlib.Tactic.RingNF.add_neg
instCharZero 📖	mathematical	—	CharZero Padic AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing	—	Rat.cast_natCast Rat.instCharZero
instCompleteSpace 📖	mathematical	—	CompleteSpace Padic PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing normedField	—	Metric.complete_of_cauchySeq_tendsto Real.instIsStrictOrderedRing Metric.cauchySeq_iff' isAbsoluteValue complete Metric.mem_nhds_iff CauSeq.equiv_lim instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
instIsUltrametricDist 📖	mathematical	—	IsUltrametricDist Padic instDist	—	Real.instIsStrictOrderedRing sub_add_sub_cancel padicNormE.nonarchimedean'
isAbsoluteValue 📖	mathematical	—	IsAbsoluteValue Real Real.semiring Real.partialOrder Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field Norm.norm instNorm	—	norm_nonneg norm_eq_zero norm_add_le map_mul AbsoluteValue.mulHomClass Rat.cast_mul IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
le_valuation_add 📖	mathematical	—	valuation Padic instAdd	—	zero_add min_le_right add_zero min_le_left nonarchimedean norm_eq_zpow_neg_valuation zpow_le_zpow_iff_right₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero Nat.Prime.one_lt Fact.out Int.instAddLeftMono covariant_swap_add_of_covariant_add
mk_eq 📖	mathematical	—	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat	—	Quotient.eq' Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat
mulValuation_toFun 📖	mathematical	—	DFunLike.coe Valuation Padic WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing instRing Valuation.instFunLike mulValuation instZero WithZero.instZero WithZero.exp valuation	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
nonarchimedean 📖	mathematical	—	Real Real.instLE Norm.norm Padic instNorm instAdd Real.instMax	—	Real.instIsStrictOrderedRing padicNormE.nonarchimedean'
norm_eq_of_norm_add_lt_left 📖	—	Real Real.instLT Norm.norm Padic instNorm instAdd	—	—	by_contradiction not_lt_of_ge add_eq_max_of_ne le_max_left
norm_eq_of_norm_add_lt_right 📖	—	Real Real.instLT Norm.norm Padic instNorm instAdd	—	—	by_contradiction not_lt_of_ge add_eq_max_of_ne le_max_right
norm_eq_of_norm_sub_lt_left 📖	—	Real Real.instLT Norm.norm Padic instNorm instSub	—	—	norm_eq_of_norm_sub_lt_right norm_neg neg_sub
norm_eq_of_norm_sub_lt_right 📖	—	Real Real.instLT Norm.norm Padic instNorm instSub	—	—	norm_neg norm_eq_of_norm_add_lt_right
norm_eq_zpow_log_mulValuation 📖	mathematical	—	Norm.norm Padic instNorm Real DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast WithZero.log Int.instAddMonoid DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing instRing Valuation.instFunLike mulValuation	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing norm_eq_zpow_neg_valuation zpow_neg WithZero.log_inv
norm_eq_zpow_neg_valuation 📖	mathematical	—	Norm.norm Padic instNorm Real DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast valuation	—	Quotient.inductionOn' Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat PadicSeq.norm_eq_zpow_neg_valuation CauSeq.not_limZero_of_not_congr_zero Mathlib.Tactic.Contrapose.contrapose₄ sub_zero Rat.cast_zpow IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Rat.cast_natCast
norm_intCast_eq_one_iff 📖	mathematical	—	Norm.norm Padic instNorm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne instRing Real Real.instOne IsCoprime Int.instCommSemiring	—	not_iff_not Nat.Prime.dvd_iff_not_coprime Fact.out norm_natAbs
norm_intCast_lt_one_iff 📖	mathematical	—	Real Real.instLT Norm.norm Padic instNorm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne instRing Real.instOne	—	Mathlib.Tactic.Contrapose.contrapose₁ le_of_eq Rat.cast_intCast eq_padicNorm Nat.cast_one Rat.cast_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing padicNorm.int_eq_one_iff Int.cast_mul Int.cast_natCast padicNormE.mul mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono le_rfl norm_int_le_one norm_nonneg mul_one norm_p inv_lt_one_of_one_lt₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.Prime.one_lt Fact.out
norm_int_le_one 📖	mathematical	—	Real Real.instLE Norm.norm Padic instNorm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne instRing Real.instOne	—	norm_rat_le_one Nat.Prime.ne_one Fact.out Rat.cast_intCast
norm_int_le_pow_iff_dvd 📖	mathematical	—	Real Real.instLE Norm.norm Padic instNorm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne instRing DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast Monoid.toNatPow Int.instMonoid	—	zpow_neg zpow_natCast Rat.cast_natCast Rat.cast_intCast instCharZero Rat.instCharZero eq_padicNorm IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing padicNorm.dvd_iff_norm_le
norm_le_one_iff_val_nonneg 📖	mathematical	—	Real Real.instLE Norm.norm Padic instNorm Real.instOne valuation	—	norm_zero Real.instZeroLEOneClass valuation_zero norm_eq_zpow_neg_valuation zpow_zero zpow_le_zpow_iff_right₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.one_lt_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero Fact.out Nat.Prime.one_lt' neg_nonpos Int.instAddLeftMono
norm_le_pow_iff_norm_lt_pow_add_one 📖	mathematical	—	Real Real.instLE Norm.norm Padic instNorm DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast Real.instLT	—	zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero Nat.Prime.pos Fact.out norm_zero le_of_lt norm_eq_zpow_neg_valuation Nat.cast_one Nat.Prime.one_lt zpow_right_strictMono₀ StrictMono.le_iff_le StrictMono.lt_iff_lt
norm_lt_pow_iff_norm_le_pow_sub_one 📖	mathematical	—	Real Real.instLT Norm.norm Padic instNorm DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast Real.instLE	—	norm_le_pow_iff_norm_lt_pow_add_one sub_add_cancel
norm_natCast_eq_one_iff 📖	mathematical	—	Norm.norm Padic instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing Real Real.instOne	—	Int.cast_natCast norm_intCast_eq_one_iff
norm_natCast_lt_one_iff 📖	mathematical	—	Real Real.instLT Norm.norm Padic instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing Real.instOne	—	Int.cast_natCast norm_intCast_lt_one_iff
norm_natCast_p_sub_one 📖	mathematical	—	Norm.norm Padic instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing Real Real.instOne	—	norm_natCast_eq_one_iff Nat.coprime_self_sub_right Nat.Prime.one_le Fact.out
norm_p 📖	mathematical	—	Norm.norm Padic instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing Real Real.instInv Real.instNatCast	—	Rat.cast_natCast padicNormE.eq_padic_norm' Rat.instCharZero Nat.Prime.ne_zero Fact.out padicValNat_self Nat.cast_one padicValNat.one Nat.cast_zero sub_zero zpow_neg zpow_one Rat.cast_inv IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
norm_p_lt_one 📖	mathematical	—	Real Real.instLT Norm.norm Padic instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing Real.instOne	—	norm_p inv_lt_one_of_one_lt₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero Nat.Prime.one_lt Fact.out
norm_p_pow 📖	mathematical	—	Norm.norm Padic instNorm Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing Real DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast	—	norm_p_zpow zpow_natCast
norm_p_zpow 📖	mathematical	—	Norm.norm Padic instNorm DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing normedField AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing Real Real.instDivInvMonoid Real.instNatCast	—	norm_zpow norm_p zpow_neg inv_zpow
norm_rat_le_one 📖	mathematical	—	Real Real.instLE Norm.norm Padic instNorm DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing normedField Real.instOne	—	Rat.zero_iff_num_zero Rat.cast_zero norm_zero Real.instZeroLEOneClass eq_padicNorm Nat.cast_one Real.instIsStrictOrderedRing padicNorm.eq_zpow_of_nonzero padicValRat.eq_1 neg_sub padicValNat.eq_zero_of_not_dvd Nat.cast_zero zero_sub zpow_neg zpow_natCast inv_le_one_of_one_le₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing Rat.instZeroLEOneClass Rat.instAddLeftMono Rat.instCharZero Nat.Prime.pos Fact.out
padicNormE_lim_le 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Norm.norm Padic instNorm IsCauSeq Real.instField Real.linearOrder Real.instIsStrictOrderedRing instRing	CauSeq.lim isAbsoluteValue complete	—	Real.instIsStrictOrderedRing isAbsoluteValue complete CauSeq.equiv_lim sub_add_cancel nonarchimedean max_le le_of_lt le_rfl
rat_dense 📖	mathematical	Real Real.instLT Real.instZero	Norm.norm Padic instNorm instSub DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing normedField	—	exists_rat_btwn Real.instIsStrictOrderedRing Real.instArchimedean rat_dense' lt_trans
rat_dense' 📖	mathematical	—	DFunLike.coe AbsoluteValue Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field Rat.semiring Rat.instPartialOrder AbsoluteValue.funLike padicNormE instSub DivisionRing.toRatCast Field.toDivisionRing	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat CauSeq.cauchy₂ PadicSeq.norm_equiv PadicSeq.stationaryPoint_spec le_rfl sub_self padicNorm.zero LT.lt.le lt_of_not_ge
valuation_intCast 📖	mathematical	—	valuation Padic AddGroupWithOne.toIntCast Ring.toAddGroupWithOne instRing padicValInt	—	Rat.cast_intCast valuation_ratCast padicValRat.of_int
valuation_inv 📖	mathematical	—	valuation Padic InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield field	—	eq_or_ne inv_zero valuation_zero neg_zero norm_inv Nat.cast_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Nat.Prime.ne_one Fact.out Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.pos Nat.instCanonicallyOrderedAdd NeZero.of_gt' Nat.Prime.one_lt' zpow_right_inj₀ IsStrictOrderedRing.toPosMulStrictMono zpow_neg norm_eq_zpow_neg_valuation inv_ne_zero
valuation_mul 📖	mathematical	—	valuation Padic instMul	—	norm_mul NormedDivisionRing.toNormMulClass Nat.cast_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Nat.Prime.ne_one Fact.out Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.pos Nat.instCanonicallyOrderedAdd NeZero.of_gt' Nat.Prime.one_lt' neg_add zpow_right_inj₀ IsStrictOrderedRing.toPosMulStrictMono zpow_add₀ LT.lt.ne' norm_eq_zpow_neg_valuation mul_ne_zero NormMulClass.toNoZeroDivisors
valuation_natCast 📖	mathematical	—	valuation Padic AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing padicValNat	—	Rat.cast_natCast valuation_ratCast padicValRat.of_nat
valuation_ofNat 📖	mathematical	—	valuation padicValNat	—	valuation_natCast
valuation_one 📖	mathematical	—	valuation Padic instOne	—	Nat.cast_one valuation_natCast padicValNat.one Nat.cast_zero
valuation_p 📖	mathematical	—	valuation Padic AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing	—	valuation_natCast padicValNat_self Nat.cast_one
valuation_pow 📖	mathematical	—	valuation Padic Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field	—	pow_zero valuation_one Nat.cast_zero MulZeroClass.zero_mul eq_or_ne zero_pow valuation_zero Nat.cast_add Nat.cast_one MulZeroClass.mul_zero pow_succ valuation_mul isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsSimpleRing.instNontrivial DivisionRing.isSimpleRing add_one_mul Distrib.rightDistribClass
valuation_ratCast 📖	mathematical	—	valuation Padic DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing normedField padicValRat	—	eq_or_ne Rat.cast_zero valuation_zero padicValRat.zero neg_injective StrictMono.injective zpow_right_strictMono₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero Nat.Prime.one_lt Fact.out norm_eq_zpow_neg_valuation Nat.cast_zero instCharZero eq_padicNorm Rat.cast_natCast Rat.cast_zpow padicNorm.eq_zpow_of_nonzero
valuation_zero 📖	mathematical	—	valuation Padic instZero	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat const_equiv
valuation_zpow 📖	mathematical	—	valuation Padic DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing normedField	—	zpow_natCast valuation_pow zpow_negSucc valuation_inv Nat.cast_add Nat.cast_one neg_add_rev IsCancelMulZero.toIsRightCancelMulZero Int.instIsCancelMulZero
zero_def 📖	mathematical	—	Padic instZero CauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm CauSeq.equiv padicNorm.instIsAbsoluteValueRat CauSeq.instZero	—	—

Padic.AddValuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add 📖	mathematical	—	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder SemilatticeInf.toMin WithTop.semilatticeInf Lattice.toSemilatticeInf instLatticeInt Padic.addValuationDef Padic Padic.instAdd	—	le_top min_eq_right zero_add le_refl min_eq_left add_zero WithTop.coe_min WithTop.coe_le_coe Padic.le_valuation_add
map_mul 📖	mathematical	—	Padic.addValuationDef Padic Padic.instMul WithTop WithTop.add	—	MulZeroClass.zero_mul WithTop.top_add MulZeroClass.mul_zero WithTop.add_top mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass WithTop.coe_add WithTop.coe_eq_coe Padic.valuation_mul
map_one 📖	mathematical	—	Padic.addValuationDef Padic Padic.instOne WithTop WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	—	Padic.addValuationDef.eq_1 one_ne_zero NeZero.charZero_one Padic.instCharZero Padic.valuation_one WithTop.coe_zero
map_zero 📖	mathematical	—	Padic.addValuationDef Padic Padic.instZero Top.top WithTop WithTop.top	—	Padic.addValuationDef.eq_1

Padic.addValuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	mathematical	—	DFunLike.coe AddValuation Padic Padic.instRing WithTop WithTop.linearOrderedAddCommMonoidWithTop AddCommGroup.toAddCancelCommMonoid Int.instAddCommGroup Int.instLinearOrder Int.instIsOrderedAddMonoid AddValuation.instFunLike Padic.addValuation WithTop.some Padic.valuation	—	Int.instIsOrderedAddMonoid

Padic.padicNormE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image 📖	mathematical	—	Norm.norm Padic Padic.instNorm Real Real.instRatCast	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat PadicSeq.ne_zero_iff_nequiv_zero PadicSeq.norm_values_discrete
is_norm 📖	mathematical	—	Real Real.instRatCast DFunLike.coe AbsoluteValue Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Padic.field Rat.semiring Rat.instPartialOrder AbsoluteValue.funLike padicNormE Norm.norm Padic.instNorm	—	—
is_rat 📖	mathematical	—	Norm.norm Padic Padic.instNorm Real Real.instRatCast	—	norm_zero Rat.cast_zero image
mul 📖	mathematical	—	Norm.norm Padic Padic.instNorm Padic.instMul Real Real.instMul	—	map_mul AbsoluteValue.mulHomClass Rat.cast_mul IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing

PadicSeq

Definitions

Name	Category	Theorems
norm 📖	CompOp	15 math math: norm_values_discrete, norm_nonneg, norm_neg, norm_nonarchimedean, norm_eq, norm_eq_of_add_equiv_zero, norm_eq_zpow_neg_valuation, norm_eq_norm_app_of_nonzero, add_eq_max_of_ne, val_eq_iff_norm_eq, norm_const, norm_one, norm_zero_iff, norm_mul, norm_equiv
stationaryPoint 📖	CompOp	3 math math: lift_index_left_left, lift_index_right, lift_index_left
valuation 📖	CompOp	2 math math: norm_eq_zpow_neg_valuation, val_eq_iff_norm_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_max_of_ne 📖	mathematical	—	norm PadicSeq CauSeq.instAdd Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat Rat.instSup	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat norm_eq_of_add_equiv_zero add_sub_cancel_right sub_zero norm_equiv norm_zero_iff max_eq_right norm_nonneg add_sub_cancel_left max_eq_left lift_index_left_left lift_index_left lift_index_right padicNorm.add_eq_max_of_ne
eq_zero_iff_equiv_zero 📖	mathematical	—	Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.Completion.Cauchy CauSeq.Completion.instZeroCauchy PadicSeq CauSeq.equiv CauSeq.instZero	—	CauSeq.Completion.mk_eq Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat
equiv_zero_of_val_eq_of_equiv_zero 📖	—	padicNorm IsCauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField PadicSeq CauSeq.equiv padicNorm.instIsAbsoluteValueRat CauSeq.instZero	—	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat sub_zero
lift_index_left 📖	mathematical	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero	IsCauSeq stationaryPoint	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat stationaryPoint_spec le_trans le_max_left le_max_right le_rfl
lift_index_left_left 📖	mathematical	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero	IsCauSeq stationaryPoint	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat stationaryPoint_spec le_max_left le_rfl
lift_index_right 📖	mathematical	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero	IsCauSeq stationaryPoint	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat stationaryPoint_spec le_trans le_max_right le_rfl
ne_zero_iff_nequiv_zero 📖	mathematical	—	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero	—	Iff.not Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat eq_zero_iff_equiv_zero
norm_const 📖	mathematical	—	norm CauSeq.const Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat eq_or_ne padicNorm.zero not_equiv_zero_const_of_nonzero
norm_eq 📖	mathematical	padicNorm IsCauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField	norm	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat equiv_zero_of_val_eq_of_equiv_zero stationaryPoint_spec le_max_left le_rfl le_max_right
norm_eq_norm_app_of_nonzero 📖	mathematical	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero	norm	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat norm_nonzero_of_not_equiv_zero padicNorm.zero
norm_eq_of_add_equiv_zero 📖	mathematical	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instAdd CauSeq.instZero	norm	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat sub_neg_eq_add sub_zero norm_equiv norm_neg
norm_eq_zpow_neg_valuation 📖	mathematical	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero	norm valuation	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat norm.eq_1 valuation.eq_1 padicNorm.eq_1 CauSeq.not_limZero_of_not_congr_zero stationaryPoint_spec le_rfl padicNorm.zero
norm_equiv 📖	mathematical	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat	norm	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat
norm_mul 📖	mathematical	—	norm PadicSeq CauSeq.instMul Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat CauSeq.mul_equiv_zero' MulZeroClass.zero_mul CauSeq.mul_equiv_zero MulZeroClass.mul_zero CauSeq.mul_not_equiv_zero lift_index_left_left lift_index_left lift_index_right padicNorm.mul
norm_neg 📖	mathematical	—	norm PadicSeq CauSeq.instNeg Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat	—	norm_eq Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat padicNorm.neg
norm_nonarchimedean 📖	mathematical	—	norm PadicSeq CauSeq.instAdd Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat Rat.instSup	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat le_max_of_le_left norm_nonneg add_sub_cancel_right sub_zero norm_equiv norm_zero_iff max_eq_right le_refl add_sub_cancel_left max_eq_left
norm_nonneg 📖	mathematical	—	norm	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat
norm_nonzero_of_not_equiv_zero 📖	—	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero	—	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat norm_zero_iff
norm_one 📖	mathematical	—	norm PadicSeq CauSeq.instOne Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat CauSeq.one_not_equiv_zero Rat.isDomain padicNorm.eq_zpow_of_nonzero NeZero.charZero_one Rat.instCharZero padicValRat.one neg_zero zpow_zero
norm_values_discrete 📖	mathematical	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero	norm	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat norm_eq_norm_app_of_nonzero zpow_neg padicNorm.values_discrete
norm_zero_iff 📖	mathematical	—	norm PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat stationaryPoint_spec le_rfl sub_zero
not_equiv_zero_const_of_nonzero 📖	mathematical	—	CauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm CauSeq.equiv padicNorm.instIsAbsoluteValueRat CauSeq.const CauSeq.instZero	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat not_limZero_const_of_nonzero sub_zero
not_limZero_const_of_nonzero 📖	mathematical	—	CauSeq.LimZero Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm CauSeq.const padicNorm.instIsAbsoluteValueRat	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat CauSeq.const_limZero
stationary 📖	mathematical	CauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm CauSeq.equiv padicNorm.instIsAbsoluteValueRat CauSeq.instZero	IsCauSeq	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat CauSeq.abv_pos_of_not_limZero CauSeq.not_limZero_of_not_congr_zero CauSeq.cauchy₂ max_le_iff lt_of_lt_of_le lt_max_iff padicNorm.add_eq_max_of_ne padicNorm.neg lt_irrefl add_comm sub_eq_add_neg max_comm
stationaryPoint_spec 📖	mathematical	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero stationaryPoint	IsCauSeq	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat stationary
val_eq_iff_norm_eq 📖	mathematical	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat CauSeq.instZero	valuation norm	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat norm_eq_zpow_neg_valuation zpow_right_inj₀ IsStrictOrderedRing.toPosMulStrictMono Rat.instZeroLEOneClass Nat.cast_zero Rat.instAddLeftMono Rat.instCharZero Nat.Prime.pos Fact.out Nat.cast_one Nat.Prime.ne_one

Rat

Definitions

Name	Category	Theorems
padicValuation 📖	CompOp	15 math math: Padic.withValUniformEquiv_norm_le_one_iff, padicValuation_cast, padicValuation_self, Padic.comap_mulValuation_eq_padicValuation, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, padicValuation_eq_zero_iff, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, Padic.isUniformInducing_cast_withVal, Padic.coe_withValRingEquiv_symm, HeightOneSpectrum.valuation_equiv_padicValuation, Padic.norm_rat_le_one_iff_padicValuation_le_one, surjective_padicValuation, Padic.isDenseInducing_cast_withVal, padicValuation_le_one_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
padicValuation_cast 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing instNormedField Valuation.instFunLike padicValuation Int.instRing Int.padicValuation	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
padicValuation_eq_zero_iff 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing instNormedField Valuation.instFunLike padicValuation WithZero.instZero	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing WithZero.instNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
padicValuation_le_one_iff 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing instNormedField Valuation.instFunLike padicValuation WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing num_div_den map_div₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Int.padicValuation_eq_one_iff padicValuation_cast Int.cast_natCast div_le_one₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono LE.le.eq_or_lt Int.padicValuation_le_one LT.lt.ne Nat.Prime.one_lt Fact.out Int.padicValuation_lt_one_iff Int.natCast_dvd
padicValuation_self 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing instNormedField Valuation.instFunLike padicValuation WithZero.exp	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instCharZero Nat.Prime.ne_zero Fact.out padicValRat.of_nat padicValNat_self Nat.cast_one
surjective_padicValuation 📖	mathematical	—	WithZero Multiplicative DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing instNormedField Valuation.instFunLike padicValuation	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing WithZero.instNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass le_or_gt isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass nontrivial instCharZero Nat.Prime.ne_zero Fact.out padicValRat.self_pow_inv Nat.cast_natAbs Int.cast_abs inv_inv EquivLike.toEmbeddingLike Int.instIsOrderedAddMonoid padicValRat.pow abs_eq_neg_self LT.lt.le Int.cast_neg padicValRat.of_nat padicValNat_self Nat.cast_one mul_one

(root)

Definitions

Name	Category	Theorems
PadicSeq 📖	CompOp	12 math math: PadicSeq.ne_zero_iff_nequiv_zero, PadicSeq.norm_neg, PadicSeq.norm_nonarchimedean, PadicInt.nthHomSeq_mul, Padic.mk_eq, PadicSeq.add_eq_max_of_ne, PadicInt.nthHomSeq_add, PadicInt.nthHomSeq_one, PadicSeq.norm_one, PadicSeq.norm_zero_iff, PadicSeq.norm_mul, PadicSeq.eq_zero_iff_equiv_zero
padicNormE 📖	CompOp	10 math math: Padic.complete', padicNormE.nonarchimedean', padicNormE.image', padicNormE.eq_padic_norm', padicNormE.defn, padicNormE.add_eq_max_of_ne', Padic.padicNormE.is_norm, Padic.complete'', Padic.exi_rat_seq_conv, Padic.rat_dense'
«termℚ_[_]» 📖	CompOp	—

padicNormE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_max_of_ne' 📖	mathematical	—	DFunLike.coe AbsoluteValue Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Padic.field Rat.semiring Rat.instPartialOrder AbsoluteValue.funLike padicNormE Padic.instAdd Rat.instSup	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat PadicSeq.add_eq_max_of_ne
defn 📖	mathematical	—	DFunLike.coe AbsoluteValue Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Padic.field Rat.semiring Rat.instPartialOrder AbsoluteValue.funLike padicNormE Padic.instSub DivisionRing.toRatCast Field.toDivisionRing IsCauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat CauSeq.cauchy₂ Mathlib.Tactic.Push.not_forall_eq not_lt_of_ge PadicSeq.norm.eq_1 not_le_of_gt le_total PadicSeq.stationaryPoint_spec le_rfl PadicSeq.norm_equiv
eq_padic_norm' 📖	mathematical	—	DFunLike.coe AbsoluteValue Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Padic.field Rat.semiring Rat.instPartialOrder AbsoluteValue.funLike padicNormE DivisionRing.toRatCast Field.toDivisionRing padicNorm	—	PadicSeq.norm_const
image' 📖	mathematical	—	DFunLike.coe AbsoluteValue Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Padic.field Rat.semiring Rat.instPartialOrder AbsoluteValue.funLike padicNormE	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat PadicSeq.ne_zero_iff_nequiv_zero PadicSeq.norm_values_discrete
nonarchimedean' 📖	mathematical	—	DFunLike.coe AbsoluteValue Padic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Padic.field Rat.semiring Rat.instPartialOrder AbsoluteValue.funLike padicNormE Padic.instAdd Rat.instSup	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat PadicSeq.norm_nonarchimedean

---

← Back to Index