PadicIntegers

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

Statistics

Metric	Count
Definitions PadicInt, ringHom, algebra, instCoePadic, instCommRing, instInhabited, instMetricSpace, instNorm, instNormedCommRing, inv, mkUnits, ofIntSeq, subring, unitCoeff, valuation, «termℤ_[_]»	16
Theorems ringHom_apply, algebraMap_apply, coe_add, coe_eq_zero, coe_intCast, coe_mul, coe_natCast, coe_ne_zero, coe_neg, coe_one, coe_pow, coe_sub, coe_sum, coe_zero, complete, completeSpace, exists_pow_neg_lt, exists_pow_neg_lt_rat, ext, ideal_eq_span_pow_p, instCharZero, instIsAdicCompleteMaximalIdeal, instIsDiscreteValuationRing, instIsDomain, instIsLocalRing, instIsUltrametricDist, instNormMulClass, instNormOneClass, intCast_eq, inv_mul, irreducible_p, isFractionRing, isOpenEmbedding_coe, isUnit_den, isUnit_iff, le_valuation_add, maximalIdeal_eq_span_p, mem_nonunits, mem_span_pow_iff_le_valuation, mem_subring_iff, mkUnits_eq, mk_coe, mk_zero, mul_inv, nonarchimedean, norm_add_eq_max_of_ne, norm_def, norm_eq_of_norm_add_lt_left, norm_eq_of_norm_add_lt_right, norm_eq_padic_norm, norm_eq_zpow_neg_valuation, norm_intCast_eq_one_iff, norm_intCast_eq_padic_norm, norm_intCast_lt_one_iff, norm_int_le_pow_iff_dvd, norm_int_lt_one_iff_dvd, norm_le_one, norm_le_pow_iff_le_valuation, norm_le_pow_iff_mem_span_pow, norm_le_pow_iff_norm_lt_pow_add_one, norm_lt_one_add, norm_lt_one_iff_dvd, norm_lt_one_mul, 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_pow, norm_units, not_isUnit_iff, one_le_norm_iff, p_nonunit, padic_norm_e_of_padicInt, pow_p_dvd_int_iff, prime_p, unitCoeff_coe, unitCoeff_spec, val_mkUnits, valuation_coe, valuation_coe_nonneg, valuation_mul, valuation_one, valuation_p, valuation_p_pow_mul, valuation_pow, valuation_zero	87
Total	103

PadicInt

Definitions

Name	Category	Theorems
algebra 📖	CompOp	2 math math: algebraMap_apply, isFractionRing
instCoePadic 📖	CompOp	—
instCommRing 📖	CompOp	85 math math: coe_sub, lift_sub_val_mem_span, coe_zero, val_mkUnits, appr_spec, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, sub_zmodRepr_mem, cyclotomicCharacter.toZModPow, norm_p_pow, coe_eq_zero, mahlerTerm_apply, coe_sum, norm_units, irreducible_p, maximalIdeal_eq_span_p, instIsDiscreteValuationRing, algebraMap_apply, instIsLocalRing, exists_mem_range, ext_of_toZModPow, mahlerSeries_apply, WittVector.fromPadicInt_comp_toPadicInt, continuous_choose, coe_addChar_of_value_at_one, instIsDomain, norm_ascPochhammer_le, coe_adicCompletionIntegersEquiv_symm_apply, toZModPow_ofIntSeq_of_pow_dvd_sub, coe_one, Coe.ringHom_apply, coe_natCast, WittVector.fromPadicInt_comp_toPadicInt_ext, valuation_pow, coe_adicCompletionIntegersEquiv_apply, mahlerTerm_one, padic_polynomial_dist, isFractionRing, zmodRepr_spec, mk_zero, toZMod_eq_residueField_comp_residue, zmod_cast_comp_toZModPow, isUnit_iff, toZModPow_eq_iff_ext, mem_span_pow_iff_le_valuation, isUnit_den, norm_le_pow_iff_mem_span_pow, ker_toZModPow, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, instIsAdicCompleteMaximalIdeal, not_isUnit_iff, WittVector.toPadicInt_comp_fromPadicInt_ext, WittVector.toPadicInt_comp_fromPadicInt, valuation_p_pow_mul, cyclotomicCharacter.toZModPow_toFun, pow_p_dvd_int_iff, continuous_multichoose, lift_spec, p_nonunit, cyclotomicCharacter.spec, mahlerEquiv_apply, mkUnits_eq, coe_neg, ker_toZMod, mahler_apply, ideal_eq_span_pow_p, mahlerEquiv_symm_apply, mem_nonunits, unitCoeff_spec, coe_mul, coe_add, intCast_eq, unitCoeff_coe, coe_dpow_eq, coe_intCast, cast_toZModPow, prime_p, WittVector.zmodEquivTrunc_compat, val_toZMod_eq_zmodRepr, cyclotomicCharacter.continuous, existsUnique_mem_range, toZMod_spec, instCharZero, cyclotomicCharacter.toFun_spec, lift_self, coe_pow
instInhabited 📖	CompOp	—
instMetricSpace 📖	CompOp	2 math math: completeSpace, instIsUltrametricDist
instNorm 📖	CompOp	40 math math: norm_int_lt_one_iff_dvd, norm_intCast_eq_padic_norm, norm_intCast_lt_one_iff, nonarchimedean, norm_p_pow, padic_norm_e_of_padicInt, norm_units, norm_lt_one_iff_dvd, exists_mem_range_of_norm_rat_le_one, norm_natCast_zmodRepr_eq_one_iff_ne, norm_eq_zpow_neg_valuation, norm_ascPochhammer_le, norm_int_le_pow_iff_dvd, padic_polynomial_dist, one_le_norm_iff, norm_natCast_zmodRepr_eq_one_iff, isUnit_iff, limNthHom_spec, norm_le_pow_iff_norm_lt_pow_add_one, norm_intCast_eq_one_iff, norm_le_pow_iff_le_valuation, norm_le_pow_iff_mem_span_pow, norm_eq_padic_norm, norm_natCast_zmodRepr_eq, instNormOneClass, not_isUnit_iff, norm_sub_modPart, norm_p, norm_lt_pow_iff_norm_le_pow_sub_one, instNormMulClass, norm_sub_zmodRepr_lt_one, norm_add_eq_max_of_ne, norm_def, norm_natCast_eq_one_iff, norm_le_one, mem_nonunits, complete, norm_natCast_zmodRepr_eq_iff, norm_natCast_p_sub_one, norm_natCast_lt_one_iff
instNormedCommRing 📖	CompOp	98 math math: lift_sub_val_mem_span, norm_int_lt_one_iff_dvd, norm_intCast_eq_padic_norm, valuation_p, hensels_lemma, appr_spec, valuation_zero, norm_intCast_lt_one_iff, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, norm_mahlerTerm, sub_zmodRepr_mem, nonarchimedean, norm_p_pow, zmodRepr_mul, mahlerTerm_apply, irreducible_p, le_valuation_add, maximalIdeal_eq_span_p, norm_lt_one_iff_dvd, mul_inv, exists_mem_range, exists_mem_range_of_norm_rat_le_one, inv_mul, fwdDiff_tendsto_zero, compactSpace, mahlerSeries_apply, norm_natCast_zmodRepr_eq_one_iff_ne, continuous_choose, coe_addChar_of_value_at_one, mahlerSeries_apply_nat, norm_ascPochhammer_le, coe_adicCompletionIntegersEquiv_symm_apply, norm_lt_one_mul, norm_int_le_pow_iff_dvd, denseRange_natCast, norm_lt_one_add, mahler_natCast_eq, coe_adicCompletionIntegersEquiv_apply, mahlerTerm_one, padic_polynomial_dist, zmodRepr_spec, norm_natCast_zmodRepr_eq_one_iff, limNthHom_spec, continuous_addChar_of_value_at_one, continuousAddCharEquiv_of_norm_mul_symm_apply, mem_span_pow_iff_le_valuation, hasSum_mahlerSeries, norm_intCast_eq_one_iff, isUnit_den, norm_le_pow_iff_mem_span_pow, zmodRepr_natCast, valuation_one, norm_natCast_zmodRepr_eq, zmodRepr_zero, ker_toZModPow, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, hasSum_mahler, instNormOneClass, limNthHom_add, instIsAdicCompleteMaximalIdeal, totallyBounded_univ, norm_sub_modPart, norm_p, valuation_p_pow_mul, fwdDiff_mahlerSeries, zmodRepr_natCast_zmodRepr, pow_p_dvd_int_iff, continuous_multichoose, p_nonunit, instNormMulClass, limNthHom_one, norm_sub_zmodRepr_lt_one, mahlerEquiv_apply, norm_add_eq_max_of_ne, norm_mahler_eq, continuousAddCharEquiv_symm_apply, norm_natCast_eq_one_iff, mahler_apply, ideal_eq_span_pow_p, limNthHom_mul, mahlerEquiv_symm_apply, complete, denseRange_intCast, limNthHom_zero, unitCoeff_spec, norm_natCast_zmodRepr_eq_iff, instIsAddTorsionFree, coe_dpow_eq, norm_natCast_p_sub_one, prime_p, zmodRepr_natCast_of_lt, cyclotomicCharacter.continuous, existsUnique_mem_range, toZMod_spec, zmodRepr_eq_zero_iff_dvd, valuation_mul, addChar_of_value_at_one_def, norm_natCast_lt_one_iff
inv 📖	CompOp	2 math math: mul_inv, inv_mul
mkUnits 📖	CompOp	2 math math: val_mkUnits, mkUnits_eq
ofIntSeq 📖	CompOp	2 math math: toZModPow_ofIntSeq_of_pow_dvd_sub, cyclotomicCharacter.toFun_apply
subring 📖	CompOp	3 math math: mem_subring_iff, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, Coe.ringHom_apply
unitCoeff 📖	CompOp	2 math math: unitCoeff_spec, unitCoeff_coe
valuation 📖	CompOp	13 math math: valuation_p, valuation_zero, le_valuation_add, norm_eq_zpow_neg_valuation, valuation_pow, mem_span_pow_iff_le_valuation, norm_le_pow_iff_le_valuation, valuation_one, valuation_coe, valuation_p_pow_mul, unitCoeff_spec, unitCoeff_coe, valuation_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom PadicInt Padic Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Padic.field RingHom.instFunLike algebraMap algebra Real Real.instLE Norm.norm Padic.instNorm Real.instOne	—	—
coe_add 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne PadicInt Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Padic.instAdd	—	—
coe_eq_zero 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne Padic.instZero PadicInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing	—	coe_zero
coe_intCast 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne PadicInt AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing instCommRing Padic.instRing	—	—
coe_mul 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne PadicInt Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Padic.instMul	—	—
coe_natCast 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne PadicInt AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instCommRing Padic.instRing	—	—
coe_ne_zero 📖	—	—	—	—	Iff.not coe_eq_zero
coe_neg 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne PadicInt NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing instCommRing Padic.instNeg	—	—
coe_one 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne PadicInt AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instCommRing Padic.instOne	—	—
coe_pow 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne PadicInt Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Padic.field	—	—
coe_sub 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne PadicInt SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing instCommRing Padic.instSub	—	—
coe_sum 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne Finset.sum PadicInt NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Padic.normedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr
coe_zero 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne PadicInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Padic.instZero	—	—
complete 📖	mathematical	—	CauSeq.IsComplete Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing PadicInt NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing Norm.norm instNorm NormMulClass.isAbsoluteValue_norm instNormMulClass	—	Real.instIsStrictOrderedRing NormMulClass.isAbsoluteValue_norm instNormMulClass Padic.isAbsoluteValue Padic.complete Padic.padicNormE_lim_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero norm_le_one CauSeq.equiv_lim
completeSpace 📖	mathematical	—	CompleteSpace PadicInt PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace	—	isClosed_le OrderTopology.to_orderClosedTopology instOrderTopologyReal continuous_norm continuous_const IsClosed.completeSpace_coe Padic.instCompleteSpace
exists_pow_neg_lt 📖	mathematical	Real Real.instLT Real.instZero	DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast	—	exists_nat_gt Real.instIsStrictOrderedRing Real.instArchimedean inv_lt_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono zpow_pos Real.instZeroLEOneClass Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero Nat.Prime.pos Fact.out zpow_neg inv_inv zpow_natCast lt_of_lt_of_le le_of_lt Nat.Prime.one_lt
exists_pow_neg_lt_rat 📖	—	—	—	—	exists_pow_neg_lt Nat.cast_zero Real.instIsStrictOrderedRing IsStrictOrderedRing.toCharZero Rat.cast_natCast
ext 📖	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne	—	—	—
ideal_eq_span_pow_p 📖	mathematical	—	Ideal.span PadicInt CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Set Set.instSingletonSet Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	IsDiscreteValuationRing.ideal_eq_span_pow_irreducible instIsDomain instIsDiscreteValuationRing irreducible_p
instCharZero 📖	mathematical	—	CharZero PadicInt AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instCommRing	—	Nat.cast_injective Padic.instCharZero
instIsAdicCompleteMaximalIdeal 📖	mathematical	—	IsAdicComplete PadicInt instCommRing IsLocalRing.maximalIdeal CommRing.toCommSemiring instIsLocalRing NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing Semiring.toModule CommSemiring.toSemiring	—	instIsLocalRing IsDiscreteValuationRing.instIsHausdorffMaximalIdeal instIsDomain instIsDiscreteValuationRing IsScalarTower.left IsScalarTower.right maximalIdeal_eq_span_p Ideal.span_singleton_pow Ideal.instIsTwoSided_1 mul_one Real.instIsStrictOrderedRing exists_pow_neg_lt lt_of_le_of_lt neg_sub norm_neg NormMulClass.isAbsoluteValue_norm instNormMulClass complete zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instZeroLEOneClass Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero Nat.Prime.pos Fact.out CauSeq.equiv_def₃ CauSeq.equiv_lim LT.lt.le le_rfl nonarchimedean LE.le.trans sub_add_sub_cancel max_le_iff
instIsDiscreteValuationRing 📖	mathematical	—	IsDiscreteValuationRing PadicInt instCommRing instIsDomain	—	IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization instIsDomain irreducible_p mul_comm unitCoeff_spec
instIsDomain 📖	mathematical	—	IsDomain PadicInt CommSemiring.toSemiring CommRing.toCommSemiring instCommRing	—	NoZeroDivisors.to_isDomain instNontrivialOfCharZero instCharZero NormMulClass.toNoZeroDivisors instNormMulClass
instIsLocalRing 📖	mathematical	—	IsLocalRing PadicInt CommSemiring.toSemiring CommRing.toCommSemiring instCommRing	—	IsLocalRing.of_nonunits_add instNontrivialOfCharZero instCharZero norm_lt_one_add
instIsUltrametricDist 📖	mathematical	—	IsUltrametricDist PadicInt PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpace	—	IsUltrametricDist.subtype Padic.instIsUltrametricDist
instNormMulClass 📖	mathematical	—	NormMulClass PadicInt instNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	norm_mul NormedDivisionRing.toNormMulClass
instNormOneClass 📖	mathematical	—	NormOneClass PadicInt instNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	norm_def NormOneClass.norm_one NormedDivisionRing.to_normOneClass
intCast_eq 📖	mathematical	—	PadicInt AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing instCommRing	—	instCharZero
inv_mul 📖	mathematical	Norm.norm PadicInt instNorm Real Real.instOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing inv AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	mul_comm mul_inv
irreducible_p 📖	mathematical	—	Irreducible PadicInt MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	Prime.irreducible IsDomain.toIsCancelMulZero instIsDomain prime_p
isFractionRing 📖	mathematical	—	IsFractionRing PadicInt CommRing.toCommSemiring instCommRing Padic Semifield.toCommSemiring Field.toSemifield Padic.field algebra	—	algebraMap_apply isUnit_iff_ne_zero coe_ne_zero mem_nonZeroDivisors_iff_ne_zero NormMulClass.toNoZeroDivisors instNormMulClass IsLocalRing.toNontrivial instIsLocalRing Submonoid.coe_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one Right.nonneg_neg_iff covariant_swap_add_of_covariant_add Int.instAddLeftMono LT.lt.le not_le Padic.norm_le_one_iff_val_nonneg norm_zero zero_le_one Real.instZeroLEOneClass Padic.padicNormE.mul Padic.norm_p_pow Padic.norm_eq_zpow_neg_valuation zpow_add' Nat.cast_ne_zero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' neg_neg neg_add_cancel zpow_zero le_of_eq NeZero.pow isReduced_of_noZeroDivisors NeZero.charZero instCharZero map_pow map_natCast
isOpenEmbedding_coe 📖	mathematical	—	Topology.IsOpenEmbedding Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Padic.normedField	—	IsOpen.isOpenEmbedding_subtypeVal dist_eq_norm_sub sub_zero IsUltrametricDist.isOpen_closedBall Padic.instIsUltrametricDist one_ne_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
isUnit_den 📖	mathematical	Real Real.instLE Norm.norm Padic Padic.instNorm DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Padic.normedField Real.instOne	IsUnit PadicInt MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	isUnit_iff le_antisymm not_lt coe_natCast Rat.cast_natCast Padic.instCharZero Rat.cast_intCast Rat.mul_den_eq_num Padic.padicNormE.mul mul_lt_mul' IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero mul_one Nat.Prime.not_dvd_one Fact.out Int.natCast_dvd
isUnit_iff 📖	mathematical	—	IsUnit PadicInt MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Norm.norm instNorm Real Real.instOne	—	isUnit_iff_dvd_one le_antisymm norm_le_one mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg NormOneClass.norm_one instNormOneClass norm_mul instNormMulClass mul_one mul_inv inv_mul
le_valuation_add 📖	mathematical	—	valuation PadicInt Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	Nat.cast_min Int.instIsStrictOrderedRing Padic.le_valuation_add coe_ne_zero
maximalIdeal_eq_span_p 📖	mathematical	—	IsLocalRing.maximalIdeal PadicInt CommRing.toCommSemiring instCommRing instIsLocalRing Ideal.span CommSemiring.toSemiring Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	le_antisymm instIsLocalRing Ideal.mem_span_singleton norm_lt_one_iff_dvd Ideal.span_le Set.singleton_subset_iff p_nonunit
mem_nonunits 📖	mathematical	—	PadicInt Set Set.instMembership nonunits MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Real Real.instLT Norm.norm instNorm Real.instOne	—	norm_le_one
mem_span_pow_iff_le_valuation 📖	mathematical	—	PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instSingletonSet Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing valuation	—	Ideal.mem_span_singleton Mathlib.Tactic.Contrapose.contrapose₄ MulZeroClass.mul_zero valuation_p_pow_mul le_self_add Nat.instCanonicallyOrderedAdd unitCoeff_spec pow_dvd_pow
mem_subring_iff 📖	mathematical	—	Padic Subring Padic.instRing SetLike.instMembership Subring.instSetLike subring Real Real.instLE Norm.norm Padic.instNorm Real.instOne	—	—
mkUnits_eq 📖	mathematical	Norm.norm Padic Padic.instNorm Real Real.instOne	Real.instLE Units.val PadicInt MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing mkUnits	—	—
mk_coe 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne	—	Subtype.coe_eta
mk_zero 📖	mathematical	Real Real.instLE Norm.norm Padic Padic.instNorm Padic.instZero Real.instOne	PadicInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing	—	—
mul_inv 📖	mathematical	Norm.norm PadicInt instNorm Real Real.instOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing inv AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	zero_ne_one' NeZero.charZero_one Padic.instCharZero norm_zero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing norm_eq_padic_norm mul_inv_cancel₀
nonarchimedean 📖	mathematical	—	Real Real.instLE Norm.norm PadicInt instNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing Real.instMax	—	Padic.nonarchimedean
norm_add_eq_max_of_ne 📖	mathematical	—	Norm.norm PadicInt instNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing Real Real.instMax	—	Padic.add_eq_max_of_ne
norm_def 📖	mathematical	—	Norm.norm PadicInt instNorm Padic Padic.instNorm Real Real.instLE Real.instOne	—	—
norm_eq_of_norm_add_lt_left 📖	—	Real Real.instLT Norm.norm PadicInt instNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	—	by_contra not_lt_of_ge norm_add_eq_max_of_ne le_max_left
norm_eq_of_norm_add_lt_right 📖	—	Real Real.instLT Norm.norm PadicInt instNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	—	by_contra not_lt_of_ge norm_add_eq_max_of_ne le_max_right
norm_eq_padic_norm 📖	mathematical	Real Real.instLE Norm.norm Padic Padic.instNorm Real.instOne	PadicInt instNorm	—	—
norm_eq_zpow_neg_valuation 📖	mathematical	—	Norm.norm PadicInt instNorm Real DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast valuation	—	Padic.norm_eq_zpow_neg_valuation coe_ne_zero valuation_coe zpow_neg zpow_natCast
norm_intCast_eq_one_iff 📖	mathematical	—	Norm.norm PadicInt instNorm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing Real Real.instOne IsCoprime Int.instCommSemiring	—	norm_def coe_intCast Padic.norm_intCast_eq_one_iff
norm_intCast_eq_padic_norm 📖	mathematical	—	Norm.norm PadicInt instNorm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing Padic Padic.instNorm Padic.instRing	—	—
norm_intCast_lt_one_iff 📖	mathematical	—	Real Real.instLT Norm.norm PadicInt instNorm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing Real.instOne	—	norm_def coe_intCast Padic.norm_intCast_lt_one_iff
norm_int_le_pow_iff_dvd 📖	mathematical	—	Real Real.instLE Norm.norm PadicInt instNorm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast Monoid.toNatPow Int.instMonoid	—	Padic.norm_int_le_pow_iff_dvd norm_intCast_eq_padic_norm zpow_neg zpow_natCast
norm_int_lt_one_iff_dvd 📖	mathematical	—	Real Real.instLT Norm.norm PadicInt instNorm AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing Real.instOne	—	Padic.norm_intCast_lt_one_iff norm_intCast_eq_padic_norm
norm_le_one 📖	mathematical	—	Real Real.instLE Norm.norm PadicInt instNorm Real.instOne	—	—
norm_le_pow_iff_le_valuation 📖	mathematical	—	Real Real.instLE Norm.norm PadicInt instNorm DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast valuation	—	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 neg_le_neg_iff Int.instAddLeftMono covariant_swap_add_of_covariant_add Nat.cast_le Int.instZeroLEOneClass Int.instCharZero
norm_le_pow_iff_mem_span_pow 📖	mathematical	—	Real Real.instLE Norm.norm PadicInt instNorm DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instSingletonSet Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	norm_zero zpow_neg zpow_natCast PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero norm_le_pow_iff_le_valuation mem_span_pow_iff_le_valuation
norm_le_pow_iff_norm_lt_pow_add_one 📖	mathematical	—	Real Real.instLE Norm.norm PadicInt instNorm DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast Real.instLT	—	norm_def Padic.norm_le_pow_iff_norm_lt_pow_add_one
norm_lt_one_add 📖	mathematical	Real Real.instLT Norm.norm PadicInt instNorm Real.instOne	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	lt_of_le_of_lt nonarchimedean max_lt
norm_lt_one_iff_dvd 📖	mathematical	—	Real Real.instLT Norm.norm PadicInt instNorm Real.instOne semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	norm_le_pow_iff_mem_span_pow pow_one Ideal.mem_span_singleton norm_le_pow_iff_norm_lt_pow_add_one zero_add neg_add_cancel zpow_zero
norm_lt_one_mul 📖	mathematical	Real Real.instLT Norm.norm PadicInt instNorm Real.instOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	norm_mul instNormMulClass mul_lt_one_of_nonneg_of_lt_one_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_le_one norm_nonneg
norm_lt_pow_iff_norm_le_pow_sub_one 📖	mathematical	—	Real Real.instLT Norm.norm PadicInt 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 PadicInt instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing Real Real.instOne	—	norm_def coe_natCast Padic.norm_natCast_eq_one_iff
norm_natCast_lt_one_iff 📖	mathematical	—	Real Real.instLT Norm.norm PadicInt instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing Real.instOne	—	norm_def coe_natCast Padic.norm_natCast_lt_one_iff
norm_natCast_p_sub_one 📖	mathematical	—	Norm.norm PadicInt instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing Real Real.instOne	—	Padic.norm_natCast_p_sub_one
norm_p 📖	mathematical	—	Norm.norm PadicInt instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing Real Real.instInv Real.instNatCast	—	Padic.norm_p
norm_p_pow 📖	mathematical	—	Norm.norm PadicInt instNorm Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing Real DivInvMonoid.toZPow Real.instDivInvMonoid Real.instNatCast	—	norm_pow instNormOneClass instNormMulClass norm_p inv_pow zpow_neg zpow_natCast
norm_units 📖	mathematical	—	Norm.norm PadicInt instNorm Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Real Real.instOne	—	isUnit_iff
not_isUnit_iff 📖	mathematical	—	IsUnit PadicInt MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Real Real.instLT Norm.norm instNorm Real.instOne	—	mem_nonunits
one_le_norm_iff 📖	mathematical	—	Real Real.instLE Real.instOne Norm.norm PadicInt instNorm	—	Subtype.prop
p_nonunit 📖	mathematical	—	PadicInt Set Set.instMembership nonunits MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	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 mem_nonunits norm_p
padic_norm_e_of_padicInt 📖	mathematical	—	Norm.norm Padic Padic.instNorm Real Real.instLE Real.instOne PadicInt instNorm	—	—
pow_p_dvd_int_iff 📖	mathematical	—	PadicInt semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing AddGroupWithOne.toIntCast Int.instMonoid	—	Nat.cast_pow norm_int_le_pow_iff_dvd norm_le_pow_iff_mem_span_pow Ideal.mem_span_singleton
prime_p 📖	mathematical	—	Prime PadicInt CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring instCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	Ideal.span_singleton_prime NeZero.charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' instCharZero instIsLocalRing maximalIdeal_eq_span_p Ideal.IsMaximal.isPrime' IsLocalRing.maximalIdeal.isMaximal
unitCoeff_coe 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne Units.val PadicInt MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing unitCoeff Padic.instMul DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Padic.normedField AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Padic.instRing valuation	—	—
unitCoeff_spec 📖	mathematical	—	PadicInt Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing unitCoeff Monoid.toNatPow AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing valuation	—	Subtype.coe_injective unitCoeff_coe mul_assoc zpow_natCast zpow_add₀ NeZero.charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Padic.instCharZero neg_add_cancel zpow_zero mul_one
val_mkUnits 📖	mathematical	Norm.norm Padic Padic.instNorm Real Real.instOne	Units.val PadicInt MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing mkUnits Real.instLE Eq.le Real.instPreorder	—	—
valuation_coe 📖	mathematical	—	Padic.valuation Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne valuation	—	sup_of_le_left
valuation_coe_nonneg 📖	mathematical	—	Padic.valuation Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne	—	eq_or_ne Padic.valuation_zero neg_nonpos Int.instAddLeftMono zpow_le_one_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 Padic.norm_eq_zpow_neg_valuation coe_ne_zero
valuation_mul 📖	mathematical	—	valuation PadicInt Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	Nat.cast_add Padic.valuation_mul coe_ne_zero
valuation_one 📖	mathematical	—	valuation PadicInt AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	Padic.valuation_one
valuation_p 📖	mathematical	—	valuation PadicInt AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	Padic.valuation_natCast padicValNat_self Nat.cast_one
valuation_p_pow_mul 📖	mathematical	—	valuation PadicInt Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	valuation_mul NeZero.pow isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors instNormMulClass NeZero.charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' instCharZero valuation_pow valuation_p mul_one
valuation_pow 📖	mathematical	—	valuation PadicInt Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing	—	Nat.cast_mul Padic.valuation_pow
valuation_zero 📖	mathematical	—	valuation PadicInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	Padic.valuation_zero

PadicInt.Coe

Definitions

Name	Category	Theorems
ringHom 📖	CompOp	1 math math: ringHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringHom_apply 📖	mathematical	—	DFunLike.coe RingHom PadicInt Padic Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring PadicInt.instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Padic.field RingHom.instFunLike ringHom Subring Padic.instRing SetLike.instMembership Subring.instSetLike PadicInt.subring	—	Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat

(root)

Definitions

Name	Category	Theorems
PadicInt 📖	CompOp	151 math math: PadicInt.coe_sub, PadicInt.lift_sub_val_mem_span, PadicInt.norm_int_lt_one_iff_dvd, PadicInt.norm_intCast_eq_padic_norm, PadicInt.valuation_p, PadicInt.coe_zero, PadicInt.val_mkUnits, PadicInt.appr_spec, PadicInt.valuation_zero, PadicInt.norm_intCast_lt_one_iff, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, PadicInt.norm_mahlerTerm, PadicInt.sub_zmodRepr_mem, cyclotomicCharacter.toZModPow, PadicInt.nonarchimedean, PadicInt.norm_p_pow, PadicInt.coe_eq_zero, PadicInt.padic_norm_e_of_padicInt, PadicInt.zmodRepr_mul, PadicInt.mahlerTerm_apply, PadicInt.coe_sum, PadicInt.norm_units, PadicInt.irreducible_p, PadicInt.le_valuation_add, PadicInt.maximalIdeal_eq_span_p, PadicInt.norm_lt_one_iff_dvd, PadicInt.instIsDiscreteValuationRing, PadicInt.algebraMap_apply, PadicInt.instIsLocalRing, PadicInt.exists_mem_range, PadicInt.exists_mem_range_of_norm_rat_le_one, PadicInt.fwdDiff_tendsto_zero, PadicInt.ext_of_toZModPow, PadicInt.compactSpace, PadicInt.mahlerSeries_apply, WittVector.fromPadicInt_comp_toPadicInt, PadicInt.norm_natCast_zmodRepr_eq_one_iff_ne, PadicInt.continuous_choose, PadicInt.coe_addChar_of_value_at_one, PadicInt.mahlerSeries_apply_nat, PadicInt.instIsDomain, PadicInt.norm_eq_zpow_neg_valuation, PadicInt.norm_ascPochhammer_le, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub, PadicInt.coe_one, PadicInt.Coe.ringHom_apply, PadicInt.completeSpace, PadicInt.coe_natCast, PadicInt.norm_int_le_pow_iff_dvd, PadicInt.denseRange_natCast, WittVector.fromPadicInt_comp_toPadicInt_ext, PadicInt.valuation_pow, mahler_natCast_eq, PadicInt.coe_adicCompletionIntegersEquiv_apply, PadicInt.mahlerTerm_one, padic_polynomial_dist, PadicInt.isFractionRing, PadicInt.zmodRepr_spec, PadicInt.mk_zero, PadicInt.one_le_norm_iff, PadicInt.norm_natCast_zmodRepr_eq_one_iff, PadicInt.toZMod_eq_residueField_comp_residue, PadicInt.zmod_cast_comp_toZModPow, PadicInt.isUnit_iff, PadicInt.limNthHom_spec, PadicInt.continuous_addChar_of_value_at_one, PadicInt.continuousAddCharEquiv_of_norm_mul_symm_apply, PadicInt.toZModPow_eq_iff_ext, PadicInt.mem_span_pow_iff_le_valuation, PadicInt.hasSum_mahlerSeries, PadicInt.norm_le_pow_iff_norm_lt_pow_add_one, PadicInt.instIsUltrametricDist, PadicInt.norm_intCast_eq_one_iff, PadicInt.norm_le_pow_iff_le_valuation, PadicInt.isUnit_den, PadicInt.norm_le_pow_iff_mem_span_pow, PadicInt.norm_eq_padic_norm, PadicInt.zmodRepr_natCast, PadicInt.valuation_one, PadicInt.norm_natCast_zmodRepr_eq, PadicInt.zmodRepr_zero, PadicInt.ker_toZModPow, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, PadicInt.hasSum_mahler, PadicInt.instNormOneClass, PadicInt.limNthHom_add, PadicInt.instIsAdicCompleteMaximalIdeal, PadicInt.not_isUnit_iff, WittVector.toPadicInt_comp_fromPadicInt_ext, PadicInt.totallyBounded_univ, WittVector.toPadicInt_comp_fromPadicInt, PadicInt.norm_sub_modPart, PadicInt.norm_p, PadicInt.valuation_p_pow_mul, cyclotomicCharacter.toZModPow_toFun, PadicInt.fwdDiff_mahlerSeries, PadicInt.zmodRepr_natCast_zmodRepr, PadicInt.pow_p_dvd_int_iff, PadicInt.continuous_multichoose, PadicInt.lift_spec, PadicInt.norm_lt_pow_iff_norm_le_pow_sub_one, PadicInt.p_nonunit, PadicInt.instNormMulClass, PadicInt.limNthHom_one, PadicInt.norm_sub_zmodRepr_lt_one, cyclotomicCharacter.spec, PadicInt.mahlerEquiv_apply, PadicInt.norm_add_eq_max_of_ne, PadicInt.mkUnits_eq, PadicInt.norm_mahler_eq, PadicInt.continuousAddCharEquiv_symm_apply, PadicInt.coe_neg, PadicInt.norm_def, PadicInt.norm_natCast_eq_one_iff, PadicInt.ker_toZMod, mahler_apply, PadicInt.ideal_eq_span_pow_p, PadicInt.limNthHom_mul, PadicInt.norm_le_one, PadicInt.mahlerEquiv_symm_apply, PadicInt.mem_nonunits, PadicInt.complete, PadicInt.denseRange_intCast, PadicInt.limNthHom_zero, PadicInt.unitCoeff_spec, PadicInt.norm_natCast_zmodRepr_eq_iff, PadicInt.coe_mul, PadicInt.coe_add, PadicInt.intCast_eq, PadicInt.unitCoeff_coe, PadicInt.instIsAddTorsionFree, PadicInt.coe_dpow_eq, PadicInt.coe_intCast, PadicInt.norm_natCast_p_sub_one, PadicInt.cast_toZModPow, PadicInt.prime_p, WittVector.zmodEquivTrunc_compat, PadicInt.zmodRepr_natCast_of_lt, PadicInt.val_toZMod_eq_zmodRepr, cyclotomicCharacter.continuous, PadicInt.existsUnique_mem_range, PadicInt.toZMod_spec, PadicInt.instCharZero, cyclotomicCharacter.toFun_spec, PadicInt.zmodRepr_eq_zero_iff_dvd, PadicInt.lift_self, PadicInt.coe_pow, PadicInt.valuation_mul, PadicInt.addChar_of_value_at_one_def, PadicInt.norm_natCast_lt_one_iff
«termℤ_[_]» 📖	CompOp	—

---

← Back to Index