Documentation Verification Report

NormedValued

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

Statistics

Metric	Count
Definitions `instRankLeOneNNRealValuation`, `instRankOneNNRealValuation`, `toValued`, `valuation`, `norm`, `toNontriviallyNormedField`, `toNormedField`	7
Theorems `valuation_apply`, `norm_add_le`, `norm_def`, `norm_eq_zero`, `norm_nonneg`, `norm_pos_iff_valuation_pos`, `coe_valuation_eq_rankOne_hom_comp_valuation`, `instIsUltrametricDist`, `isNonarchimedean_norm`, `norm_def`, `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`	17
Total	24

NormedField

Definitions

Name	Category	Theorems
`instRankLeOneNNRealValuation` 📖	CompOp	—
`instRankOneNNRealValuation` 📖	CompOp	—
`toValued` 📖	CompOp	14 math math: `Valued.integer.exists_norm_lt_one`, `Valued.integer.norm_irreducible_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`, `Irreducible.maximalIdeal_eq_closedBall`, `Valued.integer.isUnit_iff_norm_eq_one`, `Irreducible.maximalIdeal_pow_eq_closedBall_pow`, `Valued.integer.norm_coe_unit`, `Valued.integer.exists_norm_coe_lt_one`, `Valued.integer.norm_irreducible_pos`
`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`	—	—

Valuation

Definitions

Name	Category	Theorems
`norm` 📖	CompOp	6 math math: `norm_add_le`, `PadicComplex.norm_eq_norm`, `norm_nonneg`, `PadicComplex.norm_eq_norm'`, `norm_def`, `norm_pos_iff_valuation_pos`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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`	—	`ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `StrictMono.le_iff_le` `RankOne.strictMono` `le_max_iff` `map_add_le_max'` `MonoidWithZeroHom.monoidWithZeroHomClass`
`norm_def` 📖	mathematical	—	`norm` `NNReal.toReal` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.ValueGroup₀` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DivisionRing.toRing` `Field.toDivisionRing` `instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `NNReal` `WithZero.instMulZeroOneClass` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `RankOne.hom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHomClass.toMonoidWithZeroHom` `MonoidWithZeroHom.monoidWithZeroHomClass` `MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero` `restrict`	—	—
`norm_eq_zero` 📖	mathematical	`norm` `Real` `Real.instZero`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `WithZero.instNontrivial` `Nontrivial.to_nonempty` `instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `RankOne.instIsNontrivial`
`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` `instFunLike`	—	`ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `norm_def` `NNReal.coe_zero` `NNReal.coe_lt_coe` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `StrictMono.lt_iff_lt` `RankOne.strictMono` `restrict_pos_iff`

Valued

Definitions

Name	Category	Theorems
`toNontriviallyNormedField` 📖	CompOp	—
`toNormedField` 📖	CompOp	13 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_def`, `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.ValueGroup₀` `DivisionRing.toRing` `Field.toDivisionRing` `v` `Semiring.toMonoidWithZero` `Ring.toSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom` `WithZero.instMulZeroOneClass` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `Valuation.RankOne.hom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHomClass.toMonoidWithZeroHom` `MonoidWithZeroHom.monoidWithZeroHomClass` `MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero` `Valuation.restrict`	—	`instIsUltrametricDist`
`instIsUltrametricDist` 📖	mathematical	—	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `toNormedField`	—	`LE.le.trans_eq'` `Valuation.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`	—	`Valuation.norm_add_le`

Valued.toNormedField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_def` 📖	mathematical	—	`Norm.norm` `NormedField.toNorm` `Valued.toNormedField` `NNReal.toReal` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.ValueGroup₀` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `Valued.v` `Semiring.toMonoidWithZero` `Ring.toSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `NNReal` `WithZero.instMulZeroOneClass` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `Valuation.RankOne.hom` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHomClass.toMonoidWithZeroHom` `MonoidWithZeroHom.monoidWithZeroHomClass` `MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero` `Valuation.restrict`	—	—
`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`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Valuation.restrict_le_iff` `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` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Valuation.restrict_le_iff` `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`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Valuation.restrict_lt_iff` `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` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Valuation.restrict_lt_iff` `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` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Valuation.restrict_le_iff` `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` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Valuation.restrict_lt_iff` `StrictMono.lt_iff_lt` `Valuation.RankOne.strictMono`
`setOf_mem_integer_eq_closedBall` 📖	mathematical	—	`setOf` `Subring` `Ring.toNonAssocRing` `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