RankOne

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

Statistics

Metric	Count
Definitions RankLeOne, hom', rankOne_of_exists, rankOne_of_nontrivial, RankOne, hom, ofRankLeOneStruct, rankLeOneStruct, restrict_RankOne, toRankLeOne, unit, instRankOneValueGroupWithZeroValuationOfIsNontrivialOfIsRankLeOne	12
Theorems exists_val_lt, strictMono', exists_val_lt, hom_eq_zero_iff, instIsNontrivial, isNontrivial_restrict, nontrivial, restrict_RankOne_hom_eq, 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	17
Total	29

Valuation

Definitions

Name	Category	Theorems
RankLeOne 📖	CompData	—
RankOne 📖	CompData	1 math math: nonempty_rankOne_iff_mulArchimedean

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_rankOne_iff_mulArchimedean 📖	mathematical	—	RankOne MulArchimedean MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass CommMonoidWithZero.toCommMonoid WithZero.instCommMonoidWithZero Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup CommGroup.toCommMonoid Subgroup.toCommGroup Units.instCommGroupUnits LinearOrderedCommMonoidWithZero.toCommMonoidWithZero WithZero.instPartialOrder Subtype.partialOrder Units.instPartialOrderUnits SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MulArchimedean.comap RankLeOne.strictMono' Archimedean.exists_orderAddMonoidHom_real_injective Additive.isOrderedAddMonoid Units.isOrderedMonoid WithZero.isOrderedMonoid Subgroup.toIsOrderedMonoid 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.RankLeOne

Definitions

Name	Category	Theorems
hom' 📖	CompOp	4 math math: NumberField.HeightOneSpectrum.rankOne_hom'_def, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, exists_val_lt, strictMono'
rankOne_of_exists 📖	CompOp	—
rankOne_of_nontrivial 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_val_lt 📖	mathematical	—	Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder DFunLike.coe MonoidWithZeroHom Ring.toSemiring WithZero.instMulZeroOneClass Monoid.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring NNReal.instSemiring MonoidWithZeroHom.funLike hom' MonoidWithZero.toMulZeroOneClass MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.RankOne.exists_val_lt
strictMono' 📖	mathematical	—	StrictMono MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass NNReal 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 NNReal.instPartialOrder DFunLike.coe MonoidWithZeroHom WithZero.instMulZeroOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring NNReal.instSemiring MonoidWithZeroHom.funLike hom'	—	—

Valuation.RankOne

Definitions

Name	Category	Theorems
hom 📖	CompOp	8 math math: exists_val_lt, strictMono, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, PadicComplex.RankOne.hom_eq_embedding, Valued.toNormedField.norm_def, Valuation.norm_def, hom_eq_zero_iff, restrict_RankOne_hom_eq
ofRankLeOneStruct 📖	CompOp	—
rankLeOneStruct 📖	CompOp	—
restrict_RankOne 📖	CompOp	1 math math: restrict_RankOne_hom_eq
toRankLeOne 📖	CompOp	2 math math: NumberField.HeightOneSpectrum.rankOne_hom'_def, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def
unit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_val_lt 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass 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 hom MonoidWithZero.toMulZeroOneClass MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	pos_iff_ne_zero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Subgroup.toIsOrderedMonoid Units.isOrderedMonoid MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid NNReal.exists_lt_of_strictMono WithZero.instNontrivialUnits Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial isNontrivial_restrict instIsNontrivial strictMono MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective WithZero.instNontrivial Nontrivial.to_nonempty Valuation.zero_iff GroupWithZero.toNontrivial MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
hom_eq_zero_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike 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 hom NNReal.instZero WithZero.instZero	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass zero_of_hom_zero map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass
instIsNontrivial 📖	mathematical	—	Valuation.IsNontrivial LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	—	nontrivial
isNontrivial_restrict 📖	mathematical	—	Valuation.IsNontrivial MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.IsNontrivial.exists_val_nontrivial
nontrivial 📖	—	—	—	—	Valuation.IsNontrivial.exists_val_nontrivial toIsNontrivial
restrict_RankOne_hom_eq 📖	mathematical	—	hom MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Valuation.restrict restrict_RankOne MonoidWithZeroHom.comp WithZero.instGroupWithZero Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subgroup.toGroup NNReal WithZero.instMulZeroOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid NNReal.instSemiring MonoidWithZeroHom.ValueGroup₀.embedding	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass
strictMono 📖	mathematical	—	StrictMono MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass NNReal 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 NNReal.instPartialOrder DFunLike.coe MonoidWithZeroHom WithZero.instMulZeroOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring NNReal.instSemiring MonoidWithZeroHom.funLike hom	—	Valuation.RankLeOne.strictMono'
toIsNontrivial 📖	mathematical	—	Valuation.IsNontrivial LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	—	—
unit_ne_one 📖	—	—	—	—	Units.val_one nontrivial
zero_of_hom_zero 📖	mathematical	DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike 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 hom NNReal.instZero	MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithZero.instZero Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass IsOrderedMonoid.toIsOrderedCancelMonoid Subgroup.toIsOrderedMonoid Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid 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 ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.ValueGroup₀.embedding_strictMono 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 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 ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass StrictMono.comp MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.embedding_strictMono ValuativeRel.ValueGroupWithZero.embed_strictMono

(root)

Definitions

Name	Category	Theorems
instRankOneValueGroupWithZeroValuationOfIsNontrivialOfIsRankLeOne 📖	CompOp	—

---

← Back to Index