Documentation Verification Report

RankOne

📁 Source: Mathlib/RingTheory/Valuation/RankOne.lean

Statistics

Metric	Count
Definitions `RankOne`, `hom`, `ofRankLeOneStruct`, `rankLeOneStruct`, `unit`, `instRankOneValueGroupWithZeroValuationOfIsNontrivialOfIsRankLeOne`	6
Theorems `hom_eq_zero_iff`, `instIsNontrivial`, `nontrivial`, `strictMono`, `strictMono'`, `toIsNontrivial`, `unit_ne_one`, `zero_of_hom_zero`, `nonempty_rankOne_iff_mulArchimedean`, `of_compatible_mulArchimedean`, `isNontrivial_of_rankOne`, `isRankLeOne_iff_mulArchimedean`, `isRankLeOne_of_rankOne`	13
Total	19

Valuation

Definitions

Name	Category	Theorems
`RankOne` 📖	CompData	1 math math: `nonempty_rankOne_iff_mulArchimedean`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_rankOne_iff_mulArchimedean` 📖	mathematical	—	`RankOne` `MulArchimedean` `CommMonoidWithZero.toCommMonoid` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder`	—	`MulArchimedean.comap` `NNReal.instMulArchimedean` `Archimedean.exists_orderAddMonoidHom_real_injective` `Additive.isOrderedAddMonoid` `Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `Additive.instArchimedean` `Units.instMulArchimedean` `OrderAddMonoidHom.instAddMonoidHomClass` `StrictMono.comp` `strictMono_id` `Monotone.strictMono_of_injective` `OrderAddMonoidHom.monotone'` `Nat.instAtLeastTwoHAddOfNat` `le_of_lt` `Real.rpow_pos_of_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `ne_of_gt` `Real.instZeroLEOneClass` `Real.rpow_zero` `Units.ext_iff` `WithZero.log_mul` `Real.rpow_add` `WithZero.map'_strictMono` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `RCLike.charZero_rclike` `WithZero.withZeroUnitsEquiv_strictMono` `WithZero.withZeroUnitsEquiv_symm_strictMono`

Valuation.RankOne

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	6 math math: `strictMono`, `Valued.coe_valuation_eq_rankOne_hom_comp_valuation`, `Valued.norm_def`, `strictMono'`, `PadicComplex.rankOne_hom_eq`, `hom_eq_zero_iff`
`ofRankLeOneStruct` 📖	CompOp	—
`rankLeOneStruct` 📖	CompOp	—
`unit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `NNReal` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `MonoidWithZeroHom.funLike` `hom` `instZeroNNReal` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass`	—	`zero_of_hom_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`instIsNontrivial` 📖	mathematical	—	`Valuation.IsNontrivial` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	`nontrivial`
`nontrivial` 📖	—	—	—	—	`Valuation.IsNontrivial.exists_val_nontrivial` `toIsNontrivial`
`strictMono` 📖	mathematical	—	`StrictMono` `NNReal` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `instPartialOrderNNReal` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `MonoidWithZeroHom.funLike` `hom`	—	`strictMono'`
`strictMono'` 📖	mathematical	—	`StrictMono` `NNReal` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `instPartialOrderNNReal` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `MonoidWithZeroHom.funLike` `hom`	—	—
`toIsNontrivial` 📖	mathematical	—	`Valuation.IsNontrivial` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	—
`unit_ne_one` 📖	—	—	—	—	`Units.val_one` `nontrivial`
`zero_of_hom_zero` 📖	mathematical	`DFunLike.coe` `MonoidWithZeroHom` `NNReal` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `MonoidWithZeroHom.funLike` `hom` `instZeroNNReal`	`MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass`	—	`eq_of_le_of_not_lt` `zero_le'` `strictMono` `LT.lt.false` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`

ValuativeRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNontrivial_of_rankOne` 📖	mathematical	—	`IsNontrivial`	—	`isNontrivial_iff_isNontrivial` `instCompatibleValueGroupWithZeroValuation` `Valuation.RankOne.toIsNontrivial`
`isRankLeOne_iff_mulArchimedean` 📖	mathematical	—	`IsRankLeOne` `MulArchimedean` `ValueGroupWithZero` `CommMonoidWithZero.toCommMonoid` `instCommMonoidWithZeroValueGroupWithZero` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderValueGroupWithZero`	—	`MulArchimedean.comap` `NNReal.instMulArchimedean` `Valuation.nonempty_rankOne_iff_mulArchimedean` `isNontrivial_iff_isNontrivial` `instCompatibleValueGroupWithZeroValuation` `isRankLeOne_of_rankOne` `GroupWithZero.toNontrivial` `GroupWithZero.noZeroDivisors` `Mathlib.Tactic.Contrapose.contrapose₂` `eq_or_ne` `MonoidWithZeroHom.one_apply_zero` `NNReal.instCanonicallyOrderedAdd` `MonoidWithZeroHom.monoidWithZeroHomClass` `LT.lt.ne'` `LT.lt.trans'` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.one`
`isRankLeOne_of_rankOne` 📖	mathematical	—	`IsRankLeOne`	—	—

ValuativeRel.IsRankLeOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_compatible_mulArchimedean` 📖	mathematical	—	`ValuativeRel.IsRankLeOne`	—	`ValuativeRel.isRankLeOne_iff_mulArchimedean` `MulArchimedean.comap` `ValuativeRel.ValueGroupWithZero.embed_strictMono`

(root)

Definitions

Name	Category	Theorems
`instRankOneValueGroupWithZeroValuationOfIsNontrivialOfIsRankLeOne` 📖	CompOp	—

---

← Back to Index