Documentation Verification Report

RankOne

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

Statistics

Metric	Count
Definitions `rankOne`, `valueGroup₀_equiv_withZeroMulInt`	2
Theorems `generator_eq_neg_exp_one_of_surjective`, `valueGroup₀_equiv_withZeroMulInt_apply`, `valueGroup₀_equiv_withZeroMulInt_apply_zero`, `valueGroup₀_equiv_withZeroMulInt_apply_zpow`, `valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective`, `valueGroup₀_equiv_withZeroMulInt_strictMono`, `valueGroup₀_equiv_withZeroMulInt_symm_apply`	7
Total	9

Valuation.IsRankOneDiscrete

Definitions

Name	Category	Theorems
`rankOne` 📖	CompOp	—
`valueGroup₀_equiv_withZeroMulInt` 📖	CompOp	8 math math: `valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective`, `NumberField.HeightOneSpectrum.rankOne_hom'_def`, `valueGroup₀_equiv_withZeroMulInt_strictMono`, `NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def`, `valueGroup₀_equiv_withZeroMulInt_symm_apply`, `valueGroup₀_equiv_withZeroMulInt_apply`, `valueGroup₀_equiv_withZeroMulInt_apply_zero`, `valueGroup₀_equiv_withZeroMulInt_apply_zpow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`generator_eq_neg_exp_one_of_surjective` 📖	mathematical	`WithZero` `Multiplicative` `DFunLike.coe` `Valuation` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instIsStrictOrderedRing` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike`	`generator` `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` `DivisionRing.toRing` `Field.toDivisionRing` `WithZero.instGroupWithZero` `Multiplicative.group` `Int.instAddGroup` `WithZero.exp`	—	`Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `instIsNontrivial` `instIsCyclicSubtypeUnitsMemSubgroupValueGroup` `valueGroup_genLTOne_eq_generator` `LinearOrderedCommGroup.Subgroup.genLTOne_unique` `WithZero.isOrderedMonoid` `Units.val_lt_val` `Units.val_one` `WithZero.exp_zero` `Units.val_mk0` `Subgroup.ext` `WithZero.instNontrivial` `one_ne_zero` `NeZero.one` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `one_mul` `Units.ext` `zpow_neg` `Units.val_inv_eq_inv_val` `Units.val_zpow_eq_zpow_val` `inv_zpow'` `mul_one` `WithZero.exp_log` `inv_inv`
`valueGroup₀_equiv_withZeroMulInt_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MonoidWithZeroHom.ValueGroup₀` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `CommRing.toRing` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `WithZero` `Multiplicative` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Subgroup.mul` `Multiplicative.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `valueGroup₀_equiv_withZeroMulInt` `MonoidWithZeroHom` `WithZero.instMulZeroOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `Multiplicative.group` `Int.instAddGroup` `MonoidWithZeroHom.funLike` `WithZero.map'` `MonoidHomClass.toMonoidHom` `MulOne.toMul` `MulOneClass.toMulOne` `MulEquiv.symm` `intEquivOfZPowersEqTop` `Ring.toSemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `generator'`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass`
`valueGroup₀_equiv_withZeroMulInt_apply_zero` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MonoidWithZeroHom.ValueGroup₀` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `CommRing.toRing` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `WithZero` `Multiplicative` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Subgroup.mul` `Multiplicative.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `valueGroup₀_equiv_withZeroMulInt` `WithZero.instZero`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`valueGroup₀_equiv_withZeroMulInt_apply_zpow` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MonoidWithZeroHom.ValueGroup₀` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `CommRing.toRing` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `WithZero` `Multiplicative` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Subgroup.mul` `Multiplicative.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `valueGroup₀_equiv_withZeroMulInt` `Ring.toSemiring` `WithZero.instPowInt` `Subgroup.one` `Subgroup.zpow` `WithZero.coe` `generator'` `WithZero.exp`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `map_zpow₀` `MulEquivClass.toMonoidWithZeroHomClass` `MulEquiv.instMulEquivClass` `WithZero.coe_zpow` `WithZero.exp.eq_1` `map_zpow` `MulEquivClass.instMonoidHomClass` `NoMinOrder.infinite` `Nontrivial.to_nonempty` `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `instIsNontrivial` `LinearOrderedCommGroup.to_noMinOrder` `Subgroup.toIsOrderedMonoid` `Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `generator'_zpowers_eq_top` `Subgroup.zpowers_inv` `mulintEquivOfZPowersEqTop_symm_apply_zpow` `zpow_neg` `inv_zpow'` `inv_inv`
`valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective` 📖	mathematical	`WithZero` `Multiplicative` `DFunLike.coe` `Valuation` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instIsStrictOrderedRing` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike`	`DFunLike.coe` `MulEquiv` `MonoidWithZeroHom.ValueGroup₀` `WithZero` `Multiplicative` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `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` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Subgroup.mul` `Multiplicative.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `valueGroup₀_equiv_withZeroMulInt` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHom.funLike` `MonoidWithZeroHomClass.toMonoidWithZeroHom` `MonoidWithZeroHom.monoidWithZeroHomClass` `MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero` `Valuation.restrict` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instIsStrictOrderedRing`	—	`Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `WithZero.coe_unzero` `NoMinOrder.infinite` `Nontrivial.to_nonempty` `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `instIsNontrivial` `LinearOrderedCommGroup.to_noMinOrder` `Subgroup.toIsOrderedMonoid` `Units.isOrderedMonoid` `WithZero.isOrderedMonoid` `generator'_zpowers_eq_top` `Subgroup.zpowers_inv` `MulEquiv.injective` `MulEquiv.apply_symm_apply` `Units.ext` `generator_mem_valueGroup` `inv_zpow'` `generator_eq_neg_exp_one_of_surjective` `zpow_neg` `Units.val_inv_eq_inv_val` `Units.val_zpow_eq_zpow_val` `mul_one` `inv_inv`
`valueGroup₀_equiv_withZeroMulInt_strictMono` 📖	mathematical	—	`StrictMono` `MonoidWithZeroHom.ValueGroup₀` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `CommRing.toRing` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `WithZero` `Multiplicative` `WithZero.instPreorder` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Subtype.preorder` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `Multiplicative.preorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `DFunLike.coe` `MulEquiv` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Subgroup.mul` `Multiplicative.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `valueGroup₀_equiv_withZeroMulInt`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `StrictMono.lt_iff_lt` `WithZero.map'_strictMono` `MulEquiv.strictMono_symm` `NoMinOrder.infinite` `Nontrivial.to_nonempty` `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `instIsNontrivial` `LinearOrderedCommGroup.to_noMinOrder` `Subgroup.toIsOrderedMonoid` `Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `generator'_zpowers_eq_top` `Subgroup.zpowers_inv` `mulintEquivOfZPowersEqTop_strictMono` `Left.one_lt_inv_iff` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `MulMemClass.isLeftCancelMul` `instIsLeftCancelMulOfMulLeftReflectLE` `IsOrderedCancelMonoid.toMulLeftReflectLE` `IsOrderedMonoid.toIsOrderedCancelMonoid` `IsOrderedMonoid.toMulLeftMono` `generator'_lt_one`
`valueGroup₀_equiv_withZeroMulInt_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `WithZero` `Multiplicative` `MonoidWithZeroHom.ValueGroup₀` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `CommRing.toRing` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Multiplicative.mul` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `valueGroup₀_equiv_withZeroMulInt` `MonoidWithZeroHom` `WithZero.instMulZeroOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Multiplicative.group` `Int.instAddGroup` `Subgroup.toGroup` `MonoidWithZeroHom.funLike` `WithZero.map'` `MonoidHomClass.toMonoidHom` `MulOne.toMul` `MulOneClass.toMulOne` `intEquivOfZPowersEqTop` `Ring.toSemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `generator'`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass`

---

← Back to Index