Documentation Verification Report

NormedValued

📁 Source: Mathlib/Topology/Algebra/Valued/NormedValued.lean

Statistics

Metric	Count
Definitions `instRankOneNNRealValuation`, `toValued`, `valuation`, `norm`, `toNontriviallyNormedField`, `toNormedField`	6
Theorems `valuation_apply`, `coe_valuation_eq_rankOne_hom_comp_valuation`, `instIsUltrametricDist`, `isNonarchimedean_norm`, `norm_add_le`, `norm_def`, `norm_eq_zero`, `norm_nonneg`, `norm_pos_iff_valuation_pos`, `norm_le_iff`, `norm_le_one_iff`, `norm_lt_iff`, `norm_lt_one_iff`, `one_le_norm_iff`, `one_lt_norm_iff`, `setOf_mem_integer_eq_closedBall`	16
Total	22

NormedField

Definitions

Name	Category	Theorems
`instRankOneNNRealValuation` 📖	CompOp	—
`toValued` 📖	CompOp	10 math math: `Valued.integer.exists_norm_lt_one`, `Valued.integer.norm_le_one`, `Valued.integer.coe_span_singleton_eq_closedBall`, `Valued.integer.norm_unit`, `Valued.integer.exists_nnnorm_lt_one`, `v_eq_valuation`, `Valued.integer.mem_iff`, `Valued.integer.isUnit_iff_norm_eq_one`, `Valued.integer.norm_coe_unit`, `Valued.integer.exists_norm_coe_lt_one`
`valuation` 📖	CompOp	3 math math: `Valued.coe_valuation_eq_rankOne_hom_comp_valuation`, `v_eq_valuation`, `valuation_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`valuation_apply` 📖	mathematical	—	`DFunLike.coe` `Valuation` `NNReal` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `NNReal.instLinearOrderedCommGroupWithZero` `NormedRing.toRing` `NormedCommRing.toNormedRing` `toNormedCommRing` `Valuation.instFunLike` `valuation` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing`	—	—

Valued

Definitions

Name	Category	Theorems
`norm` 📖	CompOp	5 math math: `PadicComplex.norm_def`, `norm_def`, `norm_add_le`, `norm_nonneg`, `norm_pos_iff_valuation_pos`
`toNontriviallyNormedField` 📖	CompOp	—
`toNormedField` 📖	CompOp	12 math math: `instIsUltrametricDist`, `toNormedField.norm_le_one_iff`, `coe_valuation_eq_rankOne_hom_comp_valuation`, `toNormedField.norm_le_iff`, `integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField`, `toNormedField.one_lt_norm_iff`, `isNonarchimedean_norm`, `integer.properSpace_iff_compactSpace_integer`, `toNormedField.norm_lt_iff`, `toNormedField.setOf_mem_integer_eq_closedBall`, `toNormedField.norm_lt_one_iff`, `toNormedField.one_le_norm_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_valuation_eq_rankOne_hom_comp_valuation` 📖	mathematical	—	`DFunLike.coe` `Valuation` `NNReal` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `NNReal.instLinearOrderedCommGroupWithZero` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `toNormedField` `Valuation.instFunLike` `NormedField.valuation` `instIsUltrametricDist` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `MonoidWithZeroHom.funLike` `Valuation.RankOne.hom` `DivisionRing.toRing` `Field.toDivisionRing` `v`	—	`instIsUltrametricDist`
`instIsUltrametricDist` 📖	mathematical	—	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `toNormedField`	—	`LE.le.trans_eq'` `norm_add_le` `sub_add_sub_cancel`
`isNonarchimedean_norm` 📖	mathematical	—	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `toNormedField` `Norm.norm` `NormedField.toNorm`	—	`norm_add_le`
`norm_add_le` 📖	mathematical	—	`Real` `Real.instLE` `norm` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Real.instMax`	—	`StrictMono.le_iff_le` `Valuation.RankOne.strictMono` `le_max_iff` `Valuation.map_add_le_max'`
`norm_def` 📖	mathematical	—	`norm` `NNReal.toReal` `DFunLike.coe` `MonoidWithZeroHom` `NNReal` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `MonoidWithZeroHom.funLike` `Valuation.RankOne.hom` `DivisionRing.toRing` `Field.toDivisionRing` `v` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike`	—	—
`norm_eq_zero` 📖	mathematical	`norm` `Real` `Real.instZero`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`MonoidWithZeroHom.monoidWithZeroHomClass` `GroupWithZero.toNontrivial` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass`
`norm_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `norm`	—	—
`norm_pos_iff_valuation_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `norm` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `DFunLike.coe` `Valuation` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `v`	—	`norm_def` `NNReal.coe_zero` `NNReal.coe_lt_coe` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `StrictMono.lt_iff_lt` `Valuation.RankOne.strictMono`

Valued.toNormedField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_le_iff` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedField.toNorm` `Valued.toNormedField` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `Valued.v`	—	`StrictMono.le_iff_le` `Valuation.RankOne.strictMono`
`norm_le_one_iff` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedField.toNorm` `Valued.toNormedField` `Real.instOne` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `Valued.v` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `StrictMono.le_iff_le` `Valuation.RankOne.strictMono`
`norm_lt_iff` 📖	mathematical	—	`Real` `Real.instLT` `Norm.norm` `NormedField.toNorm` `Valued.toNormedField` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `Valued.v`	—	`StrictMono.lt_iff_lt` `Valuation.RankOne.strictMono`
`norm_lt_one_iff` 📖	mathematical	—	`Real` `Real.instLT` `Norm.norm` `NormedField.toNorm` `Valued.toNormedField` `Real.instOne` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `Valued.v` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `StrictMono.lt_iff_lt` `Valuation.RankOne.strictMono`
`one_le_norm_iff` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `Norm.norm` `NormedField.toNorm` `Valued.toNormedField` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `DFunLike.coe` `Valuation` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `Valued.v`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `StrictMono.le_iff_le` `Valuation.RankOne.strictMono`
`one_lt_norm_iff` 📖	mathematical	—	`Real` `Real.instLT` `Real.instOne` `Norm.norm` `NormedField.toNorm` `Valued.toNormedField` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `DFunLike.coe` `Valuation` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `Valued.v`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `StrictMono.lt_iff_lt` `Valuation.RankOne.strictMono`
`setOf_mem_integer_eq_closedBall` 📖	mathematical	—	`setOf` `Subring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Valued.toNormedField` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `Valued.v` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real` `Real.instOne`	—	`Set.ext` `dist_zero_right`

---

← Back to Index