PadicNumbers

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

Statistics

Metric	Count
Definitions `padicValuation`, `addValuation`, `addValuationDef`, `instDist`, `instNontriviallyNormedField`, `instNorm`, `limSeq`, `metricSpace`, `mk`, `mulValuation`, `normedField`, `ratNorm`, `valuation`, `PadicSeq`, `norm`, `stationaryPoint`, `valuation`, `padicValuation`, `instAddCommGroupPadic`, `instAddPadic`, `instCommRingPadic`, `instDivPadic`, `instFieldPadic`, `instInhabitedPadic`, `instMulPadic`, `instNegPadic`, `instOnePadic`, `instRingPadic`, `instSubPadic`, `instZeroPadic`, `padicNormE`, `«termℚ_[_]»`	32
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_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'`	114
Total	146

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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `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`
`instDist` 📖	CompOp	1 math math: `instIsUltrametricDist`
`instNontriviallyNormedField` 📖	CompOp	—
`instNorm` 📖	CompOp	70 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`, `PadicInt.val_mkUnits`, `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`, `norm_eq_of_norm_sub_lt_right`, `PadicInt.algebraMap_apply`, `PadicInt.exists_mem_range_of_norm_rat_le_one`, `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`, `PadicComplex.norm_extends'`, `norm_eq_of_norm_add_lt_left`, `PadicInt.coe_adicCompletionIntegersEquiv_apply`, `norm_natCast_eq_one_iff`, `PadicInt.mk_zero`, `norm_eq_of_norm_add_lt_right`, `isAbsoluteValue`, `PadicInt.norm_eq_padic_norm`, `norm_le_one_iff_val_nonneg`, `norm_intCast_lt_one_iff`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply`, `nonarchimedean`, `padicNormE.mul`, `PadicInt.valuation_coe`, `PadicInt.norm_sub_modPart`, `norm_rat_le_one`, `rat_dense`, `PadicInt.mkUnits_eq`, `padicNormE_lim_le`, `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`, `norm_eq_of_norm_sub_lt_left`, `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`
`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	33 math math: `eq_padicNorm`, `withValUniformEquiv_norm_le_one_iff`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply`, `PadicInt.coe_sum`, `PadicInt.exists_mem_range_of_norm_rat_le_one`, `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`, `PadicInt.norm_sub_modPart`, `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`, `PadicComplex.nnnorm_extends'`, `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` `instAddPadic` `Real` `Real.instMax`	—	`IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `padicNormE.add_eq_max_of_ne'`
`coe_add` 📖	mathematical	—	`Padic` `DivisionRing.toRatCast` `Field.toDivisionRing` `instFieldPadic` `instAddPadic`	—	`Rat.cast_add` `instCharZero`
`coe_div` 📖	mathematical	—	`Padic` `DivisionRing.toRatCast` `Field.toDivisionRing` `instFieldPadic` `instDivPadic`	—	`Rat.cast_div` `instCharZero`
`coe_inj` 📖	mathematical	—	`Padic` `DivisionRing.toRatCast` `Field.toDivisionRing` `instFieldPadic`	—	`Rat.instIsStrictOrderedRing` `padicNorm.instIsAbsoluteValueRat` `const_equiv` `Quotient.eq'`
`coe_mul` 📖	mathematical	—	`Padic` `DivisionRing.toRatCast` `Field.toDivisionRing` `instFieldPadic` `instMulPadic`	—	`Rat.cast_mul` `instCharZero`
`coe_neg` 📖	mathematical	—	`Padic` `DivisionRing.toRatCast` `Field.toDivisionRing` `instFieldPadic` `instNegPadic`	—	`Rat.cast_neg`
`coe_one` 📖	mathematical	—	`Padic` `DivisionRing.toRatCast` `Field.toDivisionRing` `instFieldPadic` `instOnePadic`	—	—
`coe_sub` 📖	mathematical	—	`Padic` `DivisionRing.toRatCast` `Field.toDivisionRing` `instFieldPadic` `instSubPadic`	—	`Rat.cast_sub` `instCharZero`
`coe_zero` 📖	mathematical	—	`Padic` `DivisionRing.toRatCast` `Field.toDivisionRing` `instFieldPadic` `instZeroPadic`	—	—
`comap_mulValuation_eq_int_padicValuation` 📖	mathematical	—	`Valuation.comap` `Padic` `WithZero` `Multiplicative` `instRingPadic` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instIsStrictOrderedRing` `Int.instRing` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `instCommRingPadic` `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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `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` `instRingPadic` `Norm.norm` `instNorm` `isAbsoluteValue`	—	`Real.instIsStrictOrderedRing` `isAbsoluteValue` `Rat.instIsStrictOrderedRing` `CauSeq.isCauSeq` `Nat.cast_zero` `complete''` `exists_rat_btwn` `Real.instArchimedean` `lt_trans`
`complete'` 📖	mathematical	—	`Padic` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instFieldPadic` `Rat.semiring` `Rat.instPartialOrder` `AbsoluteValue.funLike` `padicNormE` `instSubPadic` `IsCauSeq` `Rat.instField` `Rat.linearOrder` `Rat.instIsStrictOrderedRing` `instRingPadic`	—	`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` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Rat.instAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `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	—	`Padic` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instFieldPadic` `Rat.semiring` `Rat.instPartialOrder` `AbsoluteValue.funLike` `padicNormE` `instSubPadic` `IsCauSeq` `Rat.instField` `Rat.linearOrder` `Rat.instIsStrictOrderedRing` `instRingPadic`	—	`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_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` `instFieldPadic` `Rat.semiring` `Rat.instPartialOrder` `AbsoluteValue.funLike` `padicNormE` `instSubPadic` `IsCauSeq` `Rat.instField` `Rat.linearOrder` `Rat.instIsStrictOrderedRing` `instRingPadic` `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` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Rat.instAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `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.add_assoc_rev` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.add_neg` `add_zero`
`instCharZero` 📖	mathematical	—	`CharZero` `Padic` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRingPadic`	—	`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` `instFieldPadic` `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` `instAddPadic`	—	`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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instIsStrictOrderedRing` `instRingPadic` `Valuation.instFunLike` `mulValuation` `instZeroPadic` `WithZero.instZero` `WithZero.exp` `valuation`	—	`Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing`
`nonarchimedean` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Padic` `instNorm` `instAddPadic` `Real.instMax`	—	`Real.instIsStrictOrderedRing` `padicNormE.nonarchimedean'`
`norm_eq_of_norm_add_lt_left` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Padic` `instNorm` `instAddPadic`	`Norm.norm` `Padic` `instNorm`	—	`by_contradiction` `not_lt_of_ge` `add_eq_max_of_ne` `le_max_left`
`norm_eq_of_norm_add_lt_right` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Padic` `instNorm` `instAddPadic`	`Norm.norm` `Padic` `instNorm`	—	`by_contradiction` `not_lt_of_ge` `add_eq_max_of_ne` `le_max_right`
`norm_eq_of_norm_sub_lt_left` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Padic` `instNorm` `instSubPadic`	`Norm.norm` `Padic` `instNorm`	—	`norm_eq_of_norm_sub_lt_right` `norm_neg` `neg_sub`
`norm_eq_of_norm_sub_lt_right` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Padic` `instNorm` `instSubPadic`	`Norm.norm` `Padic` `instNorm`	—	`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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instIsStrictOrderedRing` `instRingPadic` `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`	—	`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` `instRingPadic` `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` `instRingPadic` `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` `instRingPadic` `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` `instRingPadic` `DivInvMonoid.toZPow` `Real.instDivInvMonoid` `Real.instNatCast` `Monoid.toPow` `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` `instRingPadic` `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` `instRingPadic` `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` `instRingPadic` `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` `instRingPadic` `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_right` `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` `instRingPadic` `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.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instFieldPadic` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRingPadic` `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` `instRingPadic` `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` `instRingPadic`	`Real` `Real.instLE` `Norm.norm` `Padic` `instNorm` `CauSeq.lim` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `instRingPadic` `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`	`Real` `Real.instLT` `Norm.norm` `Padic` `instNorm` `instSubPadic` `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` `instFieldPadic` `Rat.semiring` `Rat.instPartialOrder` `AbsoluteValue.funLike` `padicNormE` `instSubPadic` `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` `instRingPadic` `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` `instFieldPadic`	—	`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` `instMulPadic`	—	`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` `instRingPadic` `padicValNat`	—	`Rat.cast_natCast` `valuation_ratCast` `padicValRat.of_nat`
`valuation_ofNat` 📖	mathematical	—	`valuation` `padicValNat`	—	`valuation_natCast`
`valuation_one` 📖	mathematical	—	`valuation` `Padic` `instOnePadic`	—	`Nat.cast_one` `valuation_natCast` `padicValNat_one_right` `Nat.cast_zero`
`valuation_p` 📖	mathematical	—	`valuation` `Padic` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRingPadic`	—	`valuation_natCast` `padicValNat_self` `Nat.cast_one`
`valuation_pow` 📖	mathematical	—	`valuation` `Padic` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instFieldPadic`	—	`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` `instZeroPadic`	—	`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` `instZeroPadic` `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` `instAddPadic`	—	`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` `instMulPadic` `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` `instOnePadic` `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` `instZeroPadic` `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` `instRingPadic` `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` `instFieldPadic` `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` `instMulPadic` `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` 📖	mathematical	`padicNorm` `IsCauSeq` `Rat.instField` `Rat.linearOrder` `Rat.instIsStrictOrderedRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Rat.instNormedField` `PadicSeq` `CauSeq.equiv` `padicNorm.instIsAbsoluteValueRat` `CauSeq.instZero`	`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` `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`	`padicNorm` `IsCauSeq` `Rat.instField` `Rat.linearOrder` `Rat.instIsStrictOrderedRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Rat.instNormedField` `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`	`padicNorm` `IsCauSeq` `Rat.instField` `Rat.linearOrder` `Rat.instIsStrictOrderedRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Rat.instNormedField` `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`	`padicNorm` `IsCauSeq` `Rat.instField` `Rat.linearOrder` `Rat.instIsStrictOrderedRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Rat.instNormedField` `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` `padicNorm`	—	`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` `instReflLe`
`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`	`padicNorm` `IsCauSeq` `Rat.instField` `Rat.linearOrder` `Rat.instIsStrictOrderedRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Rat.instNormedField`	—	`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`	`padicNorm` `IsCauSeq` `Rat.instField` `Rat.linearOrder` `Rat.instIsStrictOrderedRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Rat.instNormedField`	—	`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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `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` `instMulPosStrictMonoWithZeroOfMulRightStrictMono` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `Multiplicative.isRightCancelMul` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `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	13 math math: `PadicSeq.ne_zero_iff_nequiv_zero`, `PadicSeq.norm_neg`, `PadicSeq.norm_nonarchimedean`, `PadicSeq.equiv_zero_of_val_eq_of_equiv_zero`, `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`
`instAddCommGroupPadic` 📖	CompOp	—
`instAddPadic` 📖	CompOp	11 math math: `padicNormE.nonarchimedean'`, `padicNormE.add_eq_max_of_ne'`, `Padic.AddValuation.map_add`, `Padic.le_valuation_add`, `Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv`, `Padic.nonarchimedean`, `Padic.coe_withValRingEquiv`, `Padic.coe_withValRingEquiv_symm`, `Padic.coe_add`, `Padic.add_eq_max_of_ne`, `PadicInt.coe_add`
`instCommRingPadic` 📖	CompOp	8 math math: `PadicInt.mem_subring_iff`, `Padic.instCompatibleWithZeroMultiplicativeIntMulValuation`, `Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn`, `PadicInt.Coe.ringHom_apply`, `PadicAlgCl.isAlgebraic`, `Padic.instIsRankLeOne`, `Padic.instIsNontrivial`, `Padic.comap_mulValuation_eq_int_padicValuation`
`instDivPadic` 📖	CompOp	1 math math: `Padic.coe_div`
`instFieldPadic` 📖	CompOp	45 math math: `Padic.coe_neg`, `Padic.complete'`, `PadicComplex.coe_eq`, `Padic.coe_div`, `PadicComplex.norm_eq_norm`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply`, `Padic.coe_sub`, `padicNormE.nonarchimedean'`, `padicNormE.image'`, `Padic.coe_zero`, `padicNormE.eq_padic_norm'`, `PadicInt.algebraMap_apply`, `PadicAlgCl.norm_extends`, `Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn`, `padicNormE.defn`, `padicNormE.add_eq_max_of_ne'`, `Padic.norm_p_pow`, `PadicInt.coe_adicCompletionIntegersEquiv_symm_apply`, `Padic.coe_mul`, `PadicAlgCl.instUniformContinuousConstSMulPadic`, `PadicInt.Coe.ringHom_apply`, `Padic.padicNormE.is_norm`, `PadicAlgCl.spectralNorm_eq`, `PadicComplex.norm_extends'`, `PadicInt.coe_adicCompletionIntegersEquiv_apply`, `Padic.coe_inj`, `PadicInt.isFractionRing`, `Padic.coe_one`, `PadicAlgCl.isAlgebraic`, `Padic.complete''`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `Padic.isAbsoluteValue`, `Padic.exi_rat_seq_conv`, `PadicComplex.norm_eq_norm'`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply`, `Padic.valuation_pow`, `Padic.rat_dense'`, `Padic.coe_add`, `PadicAlgCl.coe_eq`, `PadicComplex.nnnorm_extends'`, `PadicInt.coe_dpow_eq`, `PadicComplexInt.integers`, `PadicInt.coe_pow`, `PadicComplex.isAlgClosed`, `Padic.valuation_inv`
`instInhabitedPadic` 📖	CompOp	—
`instMulPadic` 📖	CompOp	10 math math: `Padic.coe_mul`, `Padic.valuation_mul`, `Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv`, `Padic.padicNormE.mul`, `Padic.coe_withValRingEquiv`, `Padic.AddValuation.map_mul`, `Padic.coe_withValRingEquiv_symm`, `PadicInt.coe_mul`, `PadicInt.unitCoeff_coe`, `PadicInt.coe_dpow_eq`
`instNegPadic` 📖	CompOp	2 math math: `Padic.coe_neg`, `PadicInt.coe_neg`
`instOnePadic` 📖	CompOp	4 math math: `Padic.AddValuation.map_one`, `PadicInt.coe_one`, `Padic.valuation_one`, `Padic.coe_one`
`instRingPadic` 📖	CompOp	30 math math: `PadicInt.norm_intCast_eq_padic_norm`, `Padic.norm_intCast_eq_one_iff`, `Padic.complete'`, `Padic.norm_int_le_one`, `Padic.addValuation.apply`, `Padic.instCharZero`, `Padic.norm_eq_zpow_log_mulValuation`, `Padic.valuation_p`, `Padic.norm_natCast_lt_one_iff`, `Padic.norm_p_pow`, `Padic.norm_p_lt_one`, `Padic.mulValuation_toFun`, `PadicInt.coe_natCast`, `Padic.norm_natCast_eq_one_iff`, `Padic.valuation_p_lt_one`, `Padic.complete''`, `Padic.exi_rat_seq_conv`, `Padic.valuation_intCast`, `Padic.norm_intCast_lt_one_iff`, `Padic.comap_mulValuation_eq_int_padicValuation`, `Padic.padicNormE_lim_le`, `Padic.valuation_natCast`, `Padic.norm_p`, `Padic.norm_natCast_p_sub_one`, `Padic.complete`, `PadicInt.unitCoeff_coe`, `PadicInt.coe_dpow_eq`, `PadicInt.coe_intCast`, `Padic.norm_int_le_pow_iff_dvd`, `Padic.norm_p_zpow`
`instSubPadic` 📖	CompOp	8 math math: `PadicInt.coe_sub`, `Padic.complete'`, `Padic.coe_sub`, `padicNormE.defn`, `Padic.complete''`, `Padic.exi_rat_seq_conv`, `Padic.rat_dense`, `Padic.rat_dense'`
`instZeroPadic` 📖	CompOp	9 math math: `PadicInt.coe_zero`, `PadicInt.coe_eq_zero`, `Padic.coe_zero`, `Padic.zero_def`, `Padic.valuation_zero`, `Padic.mulValuation_toFun`, `PadicInt.mk_zero`, `Padic.AddValuation.map_zero`, `PadicInt.coe_dpow_eq`
`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` `instFieldPadic` `Rat.semiring` `Rat.instPartialOrder` `AbsoluteValue.funLike` `padicNormE` `instAddPadic` `Rat.instSup`	—	`Rat.instIsStrictOrderedRing` `padicNorm.instIsAbsoluteValueRat` `PadicSeq.add_eq_max_of_ne`
`defn` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Padic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instFieldPadic` `Rat.semiring` `Rat.instPartialOrder` `AbsoluteValue.funLike` `padicNormE` `instSubPadic` `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` `instFieldPadic` `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` `instFieldPadic` `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` `instFieldPadic` `Rat.semiring` `Rat.instPartialOrder` `AbsoluteValue.funLike` `padicNormE` `instAddPadic` `Rat.instSup`	—	`Rat.instIsStrictOrderedRing` `padicNorm.instIsAbsoluteValueRat` `PadicSeq.norm_nonarchimedean`

---

← Back to Index