WithVal

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

Statistics

Metric	Count
Definitions withValRingEquiv, withValUniformEquiv, withValIntegersRingEquiv, withValIntegersUniformEquiv	4
Theorems coe_withValRingEquiv, coe_withValRingEquiv_symm, isDenseInducing_cast_withVal, isUniformInducing_cast_withVal, norm_rat_le_one_iff_padicValuation_le_one, toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, withValUniformEquiv_cast_apply, withValUniformEquiv_norm_le_one_iff	8
Total	12

Padic

Definitions

Name	Category	Theorems
withValRingEquiv 📖	CompOp	3 math math: toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, coe_withValRingEquiv, coe_withValRingEquiv_symm
withValUniformEquiv 📖	CompOp	3 math math: withValUniformEquiv_norm_le_one_iff, toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, withValUniformEquiv_cast_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_withValRingEquiv 📖	mathematical	—	DFunLike.coe RingEquiv Valuation.Completion WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Rat.padicValuation Padic UniformSpace.Completion.mul WithVal WithVal.instRing Valued.toUniformSpace WithVal.instValued instMul instAddCompletion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WithVal.instCommRing Rat.commRing instAdd EquivLike.toFunLike RingEquiv.instEquivLike withValRingEquiv UniformSpace.Completion.extension PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedField DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Distrib.toMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing WithVal.equiv	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid
coe_withValRingEquiv_symm 📖	mathematical	—	DFunLike.coe RingEquiv Padic Valuation.Completion WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Rat.padicValuation instMul UniformSpace.Completion.mul WithVal WithVal.instRing Valued.toUniformSpace WithVal.instValued instAdd instAddCompletion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WithVal.instCommRing Rat.commRing EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm withValRingEquiv IsDenseInducing.extend UniformSpace.Completion UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedField RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithVal.instField Rat.instField DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing RingHom.instFunLike RingHom.comp Rat.semiring Rat.castHom instCharZero RingEquiv.toRingHom WithVal.equiv UniformSpace.Completion.uniformSpace isDenseInducing_cast_withVal UniformSpace.Completion.coe'	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid
isDenseInducing_cast_withVal 📖	mathematical	—	IsDenseInducing WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Rat.padicValuation Padic UniformSpace.toTopologicalSpace Valued.toUniformSpace WithVal.instRing WithVal.instValued PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedField DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithVal.instField Rat.instField DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing RingHom.instFunLike RingHom.comp Rat.semiring Rat.castHom instCharZero RingEquiv.toRingHom WithVal.equiv	—	IsUniformInducing.isDenseInducing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid instCharZero isUniformInducing_cast_withVal EquivLike.range_comp denseRange_ratCast
isUniformInducing_cast_withVal 📖	mathematical	—	IsUniformInducing WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Rat.padicValuation Padic Valued.toUniformSpace WithVal.instRing WithVal.instValued PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedField DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithVal.instField Rat.instField DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing RingHom.instFunLike RingHom.comp Rat.semiring Rat.castHom instCharZero RingEquiv.toRingHom WithVal.equiv	—	IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing Rat.nontrivial Nat.Prime.pos Fact.out PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing Real.instNontrivial Rat.instAddLeftMono Rat.instZeroLEOneClass Rat.instCharZero Nat.Prime.one_lt Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid RCLike.charZero_rclike Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid instCharZero Filter.HasBasis.isUniformInducing_iff Valued.hasBasis_uniformity Metric.uniformity_basis_dist_le_pow dist_eq_norm_sub inv_pow RingHomClass.toAddMonoidHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass eq_padicNorm Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Nat.cast_pow Rat.cast_natCast Rat.cast_inv_of_ne_zero Int.cast_pow Int.cast_natCast isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.Prime.ne_zero Rat.cast_le map_sub zpow_neg Rat.instPosMulMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono zpow_natCast zpow_right_mono₀ Nat.cast_one Nat.Prime.one_le LT.lt.le IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Units.val_mk0 Valuation.map_sub_swap WithZero.lt_log_iff_exp_lt WithZero.instNontrivial zpow_le_zpow_iff_right₀ WithZero.log_mul WithZero.log_inv Nat.cast_natAbs Int.cast_abs Int.cast_add Int.cast_neg Int.cast_one
norm_rat_le_one_iff_padicValuation_le_one 📖	mathematical	—	Real Real.instLE Norm.norm Padic instNorm DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing normedField Real.instOne 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 Rat.instNormedField Valuation.instFunLike Rat.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 Rat.padicValuation_le_one_iff Nat.Prime.coprime_iff_not_dvd Fact.out PadicInt.isUnit_iff PadicInt.isUnit_den norm_rat_le_one
toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv 📖	mathematical	—	EquivLike.toEquiv Valuation.Completion WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Rat.padicValuation Padic UniformEquiv UniformSpace.Completion.uniformSpace WithVal Valued.toUniformSpace WithVal.instRing WithVal.instValued PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedField UniformEquiv.instEquivLike withValUniformEquiv RingEquiv UniformSpace.Completion.mul instMul instAddCompletion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WithVal.instCommRing Rat.commRing instAdd RingEquiv.instEquivLike withValRingEquiv	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid
withValUniformEquiv_cast_apply 📖	mathematical	—	DFunLike.coe UniformEquiv Valuation.Completion WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Rat.padicValuation Padic UniformSpace.Completion.uniformSpace WithVal Valued.toUniformSpace WithVal.instRing WithVal.instValued PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedField EquivLike.toFunLike UniformEquiv.instEquivLike withValUniformEquiv UniformSpace.Completion.coe' DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd RingEquiv.instEquivLike WithVal.equiv	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid UniformSpace.Completion.extension_coe instCharZero T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsUniformInducing.uniformContinuous isUniformInducing_cast_withVal
withValUniformEquiv_norm_le_one_iff 📖	mathematical	—	Real Real.instLE Norm.norm Padic instNorm DFunLike.coe UniformEquiv Valuation.Completion WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Rat.padicValuation UniformSpace.Completion.uniformSpace WithVal Valued.toUniformSpace WithVal.instRing WithVal.instValued PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedField EquivLike.toFunLike UniformEquiv.instEquivLike withValUniformEquiv Real.instOne Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring DivisionRing.toRing Field.toDivisionRing WithVal.instField Rat.instField IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valuation.instFunLike Valued.v Valued.valuedCompletion WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid UniformSpace.Completion.induction_on IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Set.ext Homeomorph.isClosed_setOf_iff Valued.isClopen_closedBall one_ne_zero NeZero.one WithZero.instNontrivial dist_zero_right IsUltrametricDist.isClopen_closedBall instIsUltrametricDist NeZero.charZero_one RCLike.charZero_rclike Valued.valuedCompletion_apply WithVal.apply_equiv withValUniformEquiv_cast_apply norm_rat_le_one_iff_padicValuation_le_one

PadicInt

Definitions

Name	Category	Theorems
withValIntegersRingEquiv 📖	CompOp	—
withValIntegersUniformEquiv 📖	CompOp	—

---

← Back to Index