Padic

📁 Source: Mathlib/RingTheory/DividedPowers/Padic.lean

Statistics

Metric	Count
Definitions ofInjective, Padic, dividedPowers, dividedPowers_of_injective	4
Theorems coe_dpow_eq	1
Total	5

DividedPowers

Definitions

Name	Category	Theorems
ofInjective 📖	CompOp	—

PadicInt

Definitions

Name	Category	Theorems
dividedPowers 📖	CompOp	1 math math: coe_dpow_eq
dividedPowers_of_injective 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_dpow_eq 📖	mathematical	—	Padic Real Real.instLE Norm.norm Padic.instNorm Real.instOne DividedPowers.dpow PadicInt CommRing.toCommSemiring instCommRing Ideal.span CommSemiring.toSemiring Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing dividedPowers Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Padic.instMul Ring.inverse Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Padic.field Padic.instRing Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Padic.instZero	—	Ring.inverse_eq_inv'

(root)

Definitions

Name	Category	Theorems
Padic 📖	CompOp	121 math math: Padic.eq_ratNorm, Padic.coe_neg, PadicInt.coe_sub, PadicInt.norm_intCast_eq_padic_norm, PadicInt.mem_subring_iff, PadicInt.coe_zero, Padic.norm_intCast_eq_one_iff, Padic.eq_padicNorm, Padic.withValUniformEquiv_norm_le_one_iff, Padic.AddValuation.map_one, Padic.complete', PadicComplex.coe_eq, Padic.coe_div, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, Padic.instCompatibleWithZeroMultiplicativeIntMulValuation, Padic.coe_sub, padicNormE.nonarchimedean', PadicInt.coe_eq_zero, PadicInt.padic_norm_e_of_padicInt, PadicComplex.norm_def, PadicInt.coe_sum, padicNormE.image', Padic.coe_zero, Padic.norm_int_le_one, Padic.addValuation.apply, padicNormE.eq_padic_norm', PadicInt.algebraMap_apply, Padic.instCharZero, Padic.zero_def, Padic.norm_eq_zpow_log_mulValuation, Padic.valuation_p, PadicAlgCl.norm_extends, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, PadicInt.mk_coe, Padic.norm_natCast_lt_one_iff, padicNormE.defn, padicNormE.add_eq_max_of_ne', Padic.norm_p_pow, Padic.norm_p_lt_one, Padic.valuation_zero, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, Padic.mulValuation_toFun, Padic.instCompleteSpace, Padic.comap_mulValuation_eq_padicValuation, Padic.instIsUltrametricDist, PadicInt.coe_one, Padic.coe_mul, Padic.norm_eq_zpow_neg_valuation, Padic.AddValuation.map_add, PadicAlgCl.instUniformContinuousConstSMulPadic, PadicInt.Coe.ringHom_apply, Padic.valuation_mul, PadicInt.coe_natCast, Padic.padicNormE.is_rat, PadicInt.valuation_coe_nonneg, Padic.padicNormE.is_norm, Padic.valuation_one, PadicAlgCl.spectralNorm_eq, PadicInt.coe_adicCompletionIntegersEquiv_apply, Padic.norm_natCast_eq_one_iff, Padic.coe_inj, PadicInt.isFractionRing, Padic.coe_one, Padic.valuation_p_lt_one, PadicAlgCl.isAlgebraic, Padic.valuation_zpow, Padic.le_valuation_add, Padic.complete'', PadicComplex.instIsScalarTowerPadicPadicAlgCl, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, Padic.isAbsoluteValue, Padic.exi_rat_seq_conv, Padic.valuation_intCast, Padic.norm_le_one_iff_val_nonneg, Padic.norm_intCast_lt_one_iff, Padic.AddValuation.map_zero, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, Padic.valuation_pow, Padic.denseRange_ratCast, Padic.instIsRankLeOne, Padic.instIsNontrivial, Padic.nonarchimedean, Padic.padicNormE.mul, PadicInt.valuation_coe, Padic.valuation_ratCast, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, Padic.comap_mulValuation_eq_int_padicValuation, Padic.isUniformInducing_cast_withVal, Padic.norm_rat_le_one, Padic.rat_dense, Padic.AddValuation.map_mul, Padic.rat_dense', Padic.coe_withValRingEquiv_symm, PadicInt.coe_neg, Padic.norm_rat_le_one_iff_padicValuation_le_one, PadicInt.norm_def, Padic.coe_add, PadicInt.isOpenEmbedding_coe, Padic.norm_le_pow_iff_norm_lt_pow_add_one, PadicAlgCl.coe_eq, Padic.add_eq_max_of_ne, Padic.valuation_natCast, Padic.norm_p, Padic.norm_natCast_p_sub_one, PadicInt.coe_mul, Padic.complete, PadicInt.coe_add, Padic.norm_lt_pow_iff_norm_le_pow_sub_one, Padic.instProperSpace, PadicInt.unitCoeff_coe, PadicInt.coe_dpow_eq, PadicInt.coe_intCast, Padic.padicNormE.image, padicNorm_two_harmonic, Padic.norm_int_le_pow_iff_dvd, Padic.norm_p_zpow, Padic.isDenseInducing_cast_withVal, PadicComplexInt.integers, PadicInt.coe_pow, Padic.valuation_inv

---

← Back to Index