Documentation Verification Report

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` `PartialOrder.toPreorder` `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` `instMulPadic` `instAddCompletion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `WithVal.instCommRing` `Rat.commRing` `instAddPadic` `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` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Int.instIsOrderedAddMonoid` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Rat.instNormedField` `Rat.padicValuation` `instMulPadic` `UniformSpace.Completion.mul` `WithVal` `WithVal.instRing` `Valued.toUniformSpace` `WithVal.instValued` `instAddPadic` `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` `PartialOrder.toPreorder` `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` `PartialOrder.toPreorder` `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` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Filter.HasBasis.isUniformInducing_iff` `Valued.hasBasis_uniformity` `Metric.uniformity_basis_dist_le_pow` `dist_eq_norm_sub` `inv_pow` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `WithVal.instCharZero` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `eq_padicNorm` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `map_natCast` `Rat.padicValuation_self` `nsmul_eq_mul` `mul_one` `Valuation.restrict_def` `MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff` `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` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.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` `Valuation.restrict_lt_iff` `Units.val_mk0` `Valuation.map_sub_swap` `Valuation.restrict_lt_iff_lt_embedding` `MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos` `WithZero.lt_log_iff_exp_lt` `MonoidWithZeroHom.ValueGroup₀.embedding_unit_ne_zero` `zpow_le_zpow_iff_right₀` `WithZero.log_mul` `WithZero.instNontrivial` `One.instNonempty` `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` `PartialOrder.toPreorder` `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` `instMulPadic` `instAddCompletion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `WithVal.instCommRing` `Rat.commRing` `instAddPadic` `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` `PartialOrder.toPreorder` `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` `PartialOrder.toPreorder` `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` `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` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Valuation.restrict_le_one_iff` `Homeomorph.isClosed_setOf_iff` `Valued.isClopen_closedBall` `one_ne_zero` `NeZero.one` `WithZero.instNontrivial` `One.instNonempty` `dist_zero_right` `IsUltrametricDist.isClopen_closedBall` `instIsUltrametricDist` `NeZero.charZero_one` `RCLike.charZero_rclike` `Valued.valuedCompletion_apply` `WithVal.apply_ofVal` `withValUniformEquiv_cast_apply` `norm_rat_le_one_iff_padicValuation_le_one`

PadicInt

Definitions

Name	Category	Theorems
`withValIntegersRingEquiv` 📖	CompOp	—
`withValIntegersUniformEquiv` 📖	CompOp	—

---

← Back to Index