Basic

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

Statistics

Metric	Count
Definitions AddValuation, IsEquiv, asFun, comap, instFunLike, map, of, ofValuation, supp, toPreorder, toValuation, IsEquiv, IsNontrivial, IsTrivialOn, comap, instCommGroupWithZeroSubtypeMemSubmonoidMrange, instCommMonoidWithZeroSubtypeMemSubmonoidMrange, instFunLike, leAddSubgroup, ltAddSubgroup, map, ofAddValuation, one, supp, toAddValuation, toMonoidWithZeroHom, toPreorder, ValuationClass, instCoeTCValuationOfValuationClass	29
Theorems comap, map, ne_top, of_eq, refl, trans, val_eq, comap_comp, comap_id, ext, ext_iff, map_add, map_add', map_add_eq_of_lt_left, map_add_eq_of_lt_right, map_add_of_distinct_val, map_add_supp, map_apply, map_div, map_eq_of_lt_sub, map_inv, map_le_add, map_le_sub, map_le_sum, map_lt_add, map_lt_sum, map_lt_sum', map_mul, map_neg, map_one, map_pow, map_sub, map_sub_eq_of_lt_left, map_sub_eq_of_lt_right, map_sub_swap, map_zero, mem_supp_iff, ne_top_iff, ofValuation_apply, ofValuation_symm_eq, ofValuation_toValuation, of_apply, toValuation_apply, toValuation_ofValuation, toValuation_symm_eq, top_iff, comap, eq_one_iff_eq_one, eq_zero, isNontrivial_iff, le_one_iff_le_one, lt_iff_lt, lt_one_iff_lt_one, map, ne_zero, of_eq, one_le_iff_one_le, one_lt_iff_one_lt, pos_iff, refl, trans, val_eq, val_sub_one_lt_one_iff, exists_lt_one, exists_one_lt, exists_val_nontrivial, nontrivial_codomain, IsNontrivial_iff_exists_one_lt, eq_one, valuation_algebraMap_le_one, coe_coe, coe_ltAddSubgroup, coe_mk, comap_apply, comap_comp, comap_id, comap_supp, ext, ext_iff, instIsPrimeSuppOfNontrivialOfNoZeroDivisors, instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial, instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial, instValuationClass, isEquiv_iff_val_eq_one, isEquiv_iff_val_le_one, isEquiv_iff_val_lt_one, isEquiv_iff_val_lt_val, isEquiv_iff_val_sub_one_lt_one, isEquiv_map_self_of_strictMono, isEquiv_of_val_le_one, isEquiv_tfae, isNontrivial_iff_exists_lt_one, isNontrivial_iff_exists_unit, isNontrivial_of_isEquiv, leAddSubgroup_monotone, leAddSubgroup_zero, le_one_of_subsingleton, ltAddSubgroup_le_leAddSubgroup, ltAddSubgroup_monotone, map_add, map_add', map_add_eq_of_lt_left, map_add_eq_of_lt_right, map_add_le, map_add_le_max', map_add_lt, map_add_of_distinct_val, map_add_of_left_eq_zero, map_add_of_right_eq_zero, map_add_supp, map_apply, map_div, map_eq_of_sub_lt, map_inv, map_mul, map_neg, map_one, map_one_add_of_lt, map_one_sub_of_lt, map_pow, map_sub, map_sub_eq_of_lt_left, map_sub_eq_of_lt_right, map_sub_le, map_sub_lt, map_sub_of_left_eq_zero, map_sub_of_right_eq_zero, map_sub_swap, map_sum_eq_of_lt, map_sum_le, map_sum_lt, map_sum_lt', map_zero, mem_leAddSubgroup_iff, mem_ltAddSubgroup_iff, mem_supp_iff, ne_zero_iff, ne_zero_of_isUnit, ne_zero_of_unit, not_isNontrivial_one, ofAddValuation_apply, ofAddValuation_symm_eq, ofAddValuation_toAddValuation, one_apply_def, one_apply_eq_one_iff, one_apply_eq_zero_iff, one_apply_le_one, one_apply_lt_one_iff, one_apply_of_ne_zero, one_le_val_iff, one_lt_val_iff, pos_iff, toAddValuation_apply, toAddValuation_symm_eq, toFun_eq_coe, toMonoidWithZeroHom_coe_eq_coe, toMonoidWithZeroHom_one, toValuation_ofValuation, unit_map_eq, val_eq_one_iff, val_le_one_iff, val_le_one_or_val_inv_le_one, val_le_one_or_val_inv_lt_one, val_lt_one_iff, val_mrange_zero, zero_iff, map_add_le_max, toMonoidWithZeroHomClass	168
Total	197

AddValuation

Definitions

Name	Category	Theorems
IsEquiv 📖	MathDef	2 math math: IsEquiv.of_eq, IsEquiv.refl
asFun 📖	CompOp	—
comap 📖	CompOp	7 math math: comap_id, self_le_supp_comap, onQuot_comap_eq, IsEquiv.comap, comap_supp, comap_comp, comap_onQuot_eq
instFunLike 📖	CompOp	42 math math: IsDiscreteValuationRing.addVal_zero, map_sub_swap, map_pow, map_apply, top_iff, map_add', Padic.addValuation.apply, map_add_of_distinct_val, multiplicity_addValuation_apply, HahnSeries.addVal_le_of_coeff_ne_zero, IsDiscreteValuationRing.addVal_def', Irreducible.addVal_pow, Valuation.ofAddValuation_apply, IsDiscreteValuationRing.addVal_uniformizer, Valuation.toAddValuation_apply, map_zero, HahnSeries.addVal_apply_of_ne, IsDiscreteValuationRing.addVal_mul, IsDiscreteValuationRing.addVal_add, map_mul, IsDiscreteValuationRing.addVal_pow, map_neg, IsDiscreteValuationRing.addVal_eq_zero_iff, of_apply, map_sub, map_add_supp, toValuation_apply, IsDiscreteValuationRing.addVal_eq_top_iff, IsDiscreteValuationRing.addVal_eq_zero_of_unit, IsDiscreteValuationRing.addVal_def, mem_supp_iff, map_div, IsDiscreteValuationRing.addVal_one, IsEquiv.val_eq, IsDiscreteValuationRing.addVal_le_iff_dvd, map_add, map_one, ArchimedeanClass.addValuation_apply, HahnSeries.addVal_apply, ofValuation_apply, ext_iff, map_inv
map 📖	CompOp	2 math math: IsEquiv.map, map_apply
of 📖	CompOp	1 math math: of_apply
ofValuation 📖	CompOp	5 math math: toValuation_ofValuation, ofValuation_toValuation, toValuation_symm_eq, ofValuation_symm_eq, ofValuation_apply
supp 📖	CompOp	4 math math: self_le_supp_comap, comap_supp, mem_supp_iff, supp_quot_supp
toPreorder 📖	CompOp	—
toValuation 📖	CompOp	16 math math: ArchimedeanClass.FiniteResidueField.mk_eq_zero, ArchimedeanClass.FiniteElement.val_add, toValuation_ofValuation, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, ArchimedeanClass.FiniteElement.val_mul, ArchimedeanClass.FiniteElement.val_sub, ArchimedeanClass.FiniteResidueField.mk_eq_mk, ofValuation_toValuation, ArchimedeanClass.FiniteElement.val_zero, ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, ArchimedeanClass.FiniteResidueField.mk_ne_zero, ArchimedeanClass.FiniteElement.val_one, toValuation_apply, toValuation_symm_eq, ofValuation_symm_eq, ArchimedeanClass.FiniteElement.ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_comp 📖	mathematical	—	comap RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring	—	Valuation.comap_comp
comap_id 📖	mathematical	—	comap RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring	—	Valuation.comap_id
ext 📖	—	DFunLike.coe AddValuation instFunLike	—	—	Valuation.ext
ext_iff 📖	mathematical	—	DFunLike.coe AddValuation instFunLike	—	ext
map_add 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder SemilatticeInf.toMin DFunLike.coe AddValuation instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Valuation.map_add
map_add' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	min_le_iff map_add
map_add_eq_of_lt_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	map_add_of_distinct_val LT.lt.ne min_eq_left LT.lt.le
map_add_eq_of_lt_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	map_add_eq_of_lt_left add_comm
map_add_of_distinct_val 📖	mathematical	—	DFunLike.coe AddValuation instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder	—	Valuation.map_add_of_distinct_val
map_add_supp 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule supp	DFunLike.coe AddValuation CommRing.toRing instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Valuation.map_add_supp
map_apply 📖	mathematical	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearOrderedAddCommMonoidWithTop.toAddCommMonoid AddMonoidHom.instFunLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder LinearOrderedAddCommMonoidWithTop.toOrderTop Monotone SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	AddValuation instFunLike map	—	—
map_div 📖	mathematical	—	DFunLike.coe AddValuation DivisionRing.toRing LinearOrderedAddCommGroupWithTop.instLinearOrderedAddCommMonoidWithTop instFunLike DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub LinearOrderedAddCommGroupWithTop.toSubNegMonoid	—	map_div₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
map_eq_of_lt_sub 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	—	Valuation.map_eq_of_sub_lt
map_inv 📖	mathematical	—	DFunLike.coe AddValuation DivisionRing.toRing LinearOrderedAddCommGroupWithTop.instLinearOrderedAddCommMonoidWithTop instFunLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid LinearOrderedAddCommGroupWithTop.toSubtractionMonoid	—	map_inv₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
map_le_add 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Valuation.map_add_le
map_le_sub 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	Valuation.map_sub_le
map_le_sum 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Valuation.map_sum_le
map_lt_add 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Valuation.map_add_lt
map_lt_sum 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Valuation.map_sum_lt
map_lt_sum' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder Top.top OrderTop.toTop Preorder.toLE LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toOrderTop DFunLike.coe AddValuation instFunLike	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Valuation.map_sum_lt'
map_mul 📖	mathematical	—	DFunLike.coe AddValuation instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearOrderedAddCommMonoidWithTop.toAddCommMonoid	—	Valuation.map_mul
map_neg 📖	mathematical	—	DFunLike.coe AddValuation instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Valuation.map_neg
map_one 📖	mathematical	—	DFunLike.coe AddValuation instFunLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearOrderedAddCommMonoidWithTop.toAddCommMonoid	—	Valuation.map_one
map_pow 📖	mathematical	—	DFunLike.coe AddValuation instFunLike Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring AddMonoid.toNatSMul AddCommMonoid.toAddMonoid LinearOrderedAddCommMonoidWithTop.toAddCommMonoid	—	Valuation.map_pow
map_sub 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder SemilatticeInf.toMin DFunLike.coe AddValuation instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	Valuation.map_sub
map_sub_eq_of_lt_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sub_eq_add_neg map_add_eq_of_lt_left map_neg
map_sub_eq_of_lt_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder DFunLike.coe AddValuation instFunLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	map_sub_eq_of_lt_left map_sub_swap
map_sub_swap 📖	mathematical	—	DFunLike.coe AddValuation instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	Valuation.map_sub_swap
map_zero 📖	mathematical	—	DFunLike.coe AddValuation instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder LinearOrderedAddCommMonoidWithTop.toOrderTop	—	Valuation.map_zero
mem_supp_iff 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule supp DFunLike.coe AddValuation CommRing.toRing instFunLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder LinearOrderedAddCommMonoidWithTop.toOrderTop	—	Valuation.mem_supp_iff
ne_top_iff 📖	—	—	—	—	Valuation.ne_zero_iff Multiplicative.instNontrivial OrderDual.instNontrivial
ofValuation_apply 📖	mathematical	—	DFunLike.coe AddValuation instFunLike Equiv Valuation Multiplicative OrderDual instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual EquivLike.toFunLike Equiv.instEquivLike ofValuation OrderDual.ofDual Multiplicative.toAdd Valuation.instFunLike	—	—
ofValuation_symm_eq 📖	mathematical	—	Equiv.symm Valuation Multiplicative OrderDual instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual AddValuation ofValuation toValuation	—	—
ofValuation_toValuation 📖	mathematical	—	DFunLike.coe Equiv Valuation Multiplicative OrderDual instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual AddValuation EquivLike.toFunLike Equiv.instEquivLike ofValuation toValuation	—	—
of_apply 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder LinearOrderedAddCommMonoidWithTop.toOrderTop AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearOrderedAddCommMonoidWithTop.toAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	DFunLike.coe AddValuation instFunLike of	—	—
toValuation_apply 📖	mathematical	—	DFunLike.coe Valuation Multiplicative OrderDual instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual Valuation.instFunLike Equiv AddValuation EquivLike.toFunLike Equiv.instEquivLike toValuation Multiplicative.ofAdd OrderDual.toDual instFunLike	—	—
toValuation_ofValuation 📖	mathematical	—	DFunLike.coe Equiv AddValuation Valuation Multiplicative OrderDual instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual EquivLike.toFunLike Equiv.instEquivLike toValuation ofValuation	—	—
toValuation_symm_eq 📖	mathematical	—	Equiv.symm AddValuation Valuation Multiplicative OrderDual instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual toValuation ofValuation	—	—
top_iff 📖	mathematical	—	DFunLike.coe AddValuation DivisionRing.toRing instFunLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder LinearOrderedAddCommMonoidWithTop.toOrderTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Valuation.zero_iff Multiplicative.instNontrivial OrderDual.instNontrivial

AddValuation.IsEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	AddValuation.IsEquiv	AddValuation.comap	—	Valuation.IsEquiv.comap
map 📖	mathematical	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearOrderedAddCommMonoidWithTop.toAddCommMonoid AddMonoidHom.instFunLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder LinearOrderedAddCommMonoidWithTop.toOrderTop Monotone SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddValuation.IsEquiv	AddValuation.map	—	Valuation.IsEquiv.map AddMonoidHom.map_zero AddMonoidHom.map_add
ne_top 📖	—	AddValuation.IsEquiv	—	—	Iff.ne Valuation.IsEquiv.eq_zero
of_eq 📖	mathematical	—	AddValuation.IsEquiv	—	Valuation.IsEquiv.of_eq
refl 📖	mathematical	—	AddValuation.IsEquiv	—	Valuation.IsEquiv.refl
trans 📖	—	AddValuation.IsEquiv	—	—	Valuation.IsEquiv.trans
val_eq 📖	mathematical	AddValuation.IsEquiv	DFunLike.coe AddValuation AddValuation.instFunLike	—	Valuation.IsEquiv.val_eq

Valuation

Definitions

Name	Category	Theorems
IsEquiv 📖	MathDef	15 math math: isEquiv_iff_val_sub_one_lt_one, isEquiv_map_self_of_strictMono, isEquiv_valuation_valuationSubring, isEquiv_iff_val_lt_val, isEquiv_iff_val_le_one, isEquiv_iff_val_eq_one, isEquiv_of_val_le_one, ValuativeRel.isEquiv, HasExtension.val_isEquiv_comap, Rat.HeightOneSpectrum.valuation_equiv_padicValuation, isEquiv_tfae, isEquiv_iff_val_lt_one, IsEquiv.refl, IsEquiv.of_eq, isEquiv_iff_valuationSubring
IsNontrivial 📖	CompData	17 math math: IsEquiv.isNontrivial_iff, isNontrivial_iff_exists_lt_one, IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntValuation, FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation, ValuationSubring.eq_top_iff, ValuativeRel.isNontrivial_iff_isNontrivial, ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible, isNontrivial_iff_exists_unit, RankOne.instIsNontrivial, IsNontrivial_iff_exists_one_lt, not_isNontrivial_one, isNontrivial_valuation_valuationSubring_iff, RankOne.toIsNontrivial, valuationSubring_eq_top_iff, IsRankOneDiscrete.instIsNontrivial, isNontrivial_iff_not_a_field, isNontrivial_of_isEquiv
IsTrivialOn 📖	CompData	1 math math: FiniteField.instIsTrivialOn
comap 📖	CompOp	12 math math: Padic.comap_mulValuation_eq_padicValuation, comap_onQuot_eq, comap_id, ValuativeExtension.compatible_comap, comap_supp, comap_apply, comap_comp, HasExtension.val_isEquiv_comap, onQuot_comap_eq, Padic.comap_mulValuation_eq_int_padicValuation, self_le_supp_comap, IsEquiv.comap
instCommGroupWithZeroSubtypeMemSubmonoidMrange 📖	CompOp	—
instCommMonoidWithZeroSubtypeMemSubmonoidMrange 📖	CompOp	1 math math: val_mrange_zero
instFunLike 📖	CompOp	331 math math: Valued.isOpen_closedball, IsTrivialOn.valuation_algebraMap_le_one, Irreducible.maximalIdeal_eq_setOf_le_v_coe, ValuationSubring.valuation_lt_one_iff, leSubmodule_v_le_of_mem, FiniteField.algebraMap_le_one, FiniteField.algebraMap_eq_one, HasExtension.val_map_le_iff, isEquiv_iff_val_sub_one_lt_one, one_apply_lt_one_iff, mem_maximalIdeal_iff, val_mrange_zero, mem_leSubmodule_iff, mem_supp_iff, Padic.withValUniformEquiv_norm_le_one_iff, Valued.toNormedField.norm_le_one_iff, Rat.padicValuation_cast, Valued.extension_extends, Valued.valuedCompletion_surjective_iff, ValuativeRel.valuation_eq_zero_iff, ValuationSubring.valuation_le_iff, PadicComplex.valuation_extends, IsRankOneDiscrete.exists_generator_lt_one', IsTrivialOn.eq_one, mem_ltIdeal_iff, toFun_eq_coe, val_le_one_or_val_inv_lt_one, NumberField.FinitePlace.norm_def', IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, FunctionField.inftyValuation.X_inv, Int.padicValuation_lt_one_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, IsRankOneDiscrete.generator_mem_valueGroup, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, Integers.isPrincipal_iff_exists_isGreatest, LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, LaurentSeries.valuation_single_zpow, IsDedekindDomain.HeightOneSpectrum.intValuation_le_one, ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl, instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial, WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral, ValuationSubring.valuation_unit, Compatible.srel_iff_lt, isEquiv_iff_val_lt_val, isNontrivial_iff_exists_lt_one, Integers.valuation_irreducible_lt_one, Int.padicValuation_eq_one_iff, ValuationSubring.mapOfLE_valuation_apply, Integers.map_le_one, HasExtension.val_map_eq_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem, IsDedekindDomain.HeightOneSpectrum.intValuation_singleton, ext_iff, Rat.padicValuation_self, ltIdeal_v_le_of_mem, Valued.isClopen_ball, IsEquiv.pos_iff, Valued.exists_coe_eq_v, ValuativeRel.ValueGroupWithZero.mk_eq_div, unit_map_eq, Integers.le_of_dvd, Polynomial.valuation_of_mk, val_lt_one_iff, IsUniformizer.zpowers_eq_valueGroup, val_le_one_or_val_inv_le_one, map_add_of_distinct_val, map_add, HasExtension.val_map_lt_iff, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, map_div, one_lt_val_iff, Padic.norm_eq_zpow_log_mulValuation, ValuationSubring.valuation_lt_one_or_eq_one, PowerSeries.intValuation_eq_of_coe, one_apply_of_ne_zero, Valued.continuous_valuation, WithVal.apply_symm_equiv, val_eq_one_iff, LaurentSeries.val_le_one_iff_eq_coe, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer, IsValuativeTopology.isClopen_sphere, FunctionField.valuedFqtInfty.def, coe_coe, WithVal.apply_equiv, IsEquiv.one_lt_iff_one_lt, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, mem_unitGroup_iff, Valued.isOpen_sphere, IsDedekindDomain.HeightOneSpectrum.valuation_def, ValuationSubring.valuation_le_one, LaurentSeries.exists_ratFunc_val_lt, Valued.hasBasis_nhds_zero, IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup, IsValuativeTopology.continuous_valuation, Padic.mulValuation_toFun, IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff, IsValuativeTopology.mem_nhds_iff', IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd, map_sub_swap, isEquiv_iff_val_le_one, Integers.not_denselyOrdered_of_isPrincipalIdealRing, IsUniformizer.val, ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq, HasExtension.val_map_le_one_iff, map_sub, Rat.valuation_le_one_iff_den, mem_valuationSubring_iff, ofAddValuation_apply, Integers.isIntegral_iff_v_le_one, ValuativeExtension.mapValueGroupWithZero_valuation, isEquiv_iff_val_eq_one, Integers.isPrincipalIdealRing_iff_not_denselyOrdered, WeierstrassCurve.isGoodReduction_iff, Integers.le_iff_dvd, LaurentSeries.exists_Polynomial_intValuation_lt, Valued.continuous_extensionValuation, ValuationSubring.valuation_le_one_iff, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, ValuationSubring.mem_unitGroup_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', toAddValuation_apply, Valued.isClosed_ball, zero_iff, srel_iff_lt, Valued.isClopen_sphere, PadicAlgCl.valuation_p, PadicComplex.valuation_p, Valued.isClosed_sphere, IsValuativeTopology.isClosed_closedBall, IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, one_apply_eq_zero_iff, IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', WithVal.lt_def, IsValuativeTopology.mem_nhds_zero_iff, ModP.preVal_mk, apply_posSubmonoid_pos, one_srel_iff, RatFunc.valuation_eq_LaurentSeries_valuation, ModP.v_p_lt_preVal, IsRankOneDiscrete.generator_zpowers_eq_range, mem_leAddSubgroup_iff, vle_iff_le, Valued.toNormedField.norm_le_iff, map_add', IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, Valued.integer.mulArchimedean_mrange_of_isCompact_integer, Integers.dvdNotUnit_iff_lt, Padic.valuation_p_lt_one, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, Integers.valuation_unit, IsEquiv.lt_iff_lt, map_mul, Valued.closure_coe_completion_v_lt, Valued.valuation_isClosedMap, Int.padicValuation_self, Valued.closure_coe_completion_v_mul_v_lt, Valued.valuedCompletion_apply, Valued.cauchy_iff, one_apply_le_one, ValuationSubring.valuation_eq_iff, ValuativeRel.one_apply_posSubmonoid, instValuationClass, Valued.norm_def, comap_apply, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, NumberField.FinitePlace.norm_def_int, leIdeal_v_le_of_mem, veq_iff_eq, IsValuativeTopology.hasBasis_nhds_zero', extendToLocalization_mk', Integers.maximalIdeal_eq_setOf_le_v_algebraMap, map_one, one_vlt_iff, IsValuativeTopology.isClopen_ball, IsValuativeTopology.hasBasis_nhds, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd, one_vle_iff, Valued.toNormedField.one_lt_norm_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt, IsValuativeTopology.hasBasis_nhds_zero, IsEquiv.eq_zero, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsNontrivial_iff_exists_one_lt, mem_ltAddSubgroup_iff, IsRankOneDiscrete.generator_zpowers_eq_valueGroup, LaurentSeries.valuation_LaurentSeries_equal_extension, RatFunc.v_def, Rat.padicValuation_eq_zero_iff, map_inv, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff, Integers.wfDvdMonoid_iff_wellFounded_gt_on_v, Set.unit_valuation_eq_one, IsValuativeTopology.isOpen_closedBall, integer.v_irreducible_pos, FunctionField.inftyValuation.X_zpow, ValuativeRel.exists_valuation_div_valuation_eq, map_apply, IsNontrivial.exists_one_lt, IsDedekindDomain.HeightOneSpectrum.intValuation_def, PadicAlgCl.valuation_def, FunctionField.inftyValuation.X, toMonoidWithZeroHom_coe_eq_coe, srel_one_iff, PadicAlgCl.valuation_coe, IsUniformizer.val_pos, FunctionField.inftyValuedFqt.def, vle_one_iff, IsEquiv.val_sub_one_lt_one_iff, Integers.coe_span_singleton_eq_setOf_le_v_algebraMap, IsValuativeTopology.hasBasis_nhds', Integers.valuation_pos_iff_ne_zero, Valued.isOpen_closedBall, instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial, IsEquiv.one_le_iff_one_le, ltSubmodule_v_le_of_mem, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, Valued.mem_nhds_zero, HasExtension.val_map_eq_one_iff, Valued.isOpen_ball, ValuationSubring.mem_principalUnitGroup_iff, NormedField.v_eq_valuation, Valued.mem_nhds, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq, map_neg, IsNonarchimedeanLocalField.isCompact_closedBall, Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer, Valued.extensionValuation_apply_coe, ValuativeRel.valuation_surjective, IsDedekindDomain.HeightOneSpectrum.valuation_surjective, rel_one_iff, IsEquiv.eq_one_iff_eq_one, LaurentSeries.valuation_coe_ratFunc, ValuativeRel.ValueGroupWithZero.embed_mk, AddValuation.toValuation_apply, Integers.isPrincipal_iff_exists_eq_setOf_valuation_le, IsValuativeTopology.isClosed_ball, Integer.not_isUnit_iff_valuation_lt_one, vlt_one_iff, LaurentSeries.valuation_compare, LaurentSeries.tendsto_valuation, IsEquiv.le_one_iff_le_one, integer.coe_span_singleton_eq_setOf_le_v_coe, Integers.wellFounded_gt_on_v_iff_discrete_mrange, PowerSeries.intValuation_X, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', IsEquiv.val_eq, HasExtension.mk_smul_mk, ValuationSubring.mem_nonunits_iff, Valued.toNormedField.norm_lt_iff, map_pow, rel_iff_le, Integers.valuation_irreducible_pos, NumberField.toNNReal_valued_eq_adicAbv, vlt_iff_lt, IsUniformizer.iff, Valued.hasBasis_uniformity, mem_ltSubmodule_iff, ModP.v_p_lt_val, integer.v_irreducible_lt_one, FunctionField.inftyValuation.C, IsNontrivial.exists_lt_one, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, Integers.isUnit_iff_valuation_eq_one, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, extendToLocalization_apply_map_apply, mem_leIdeal_iff, Padic.norm_rat_le_one_iff_padicValuation_le_one, Valued.isClosed_closedBall, Set.integer_valuation_le_one, PreTilt.map_eq_zero, coe_ltAddSubgroup, Rat.surjective_padicValuation, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer, WithVal.le_def, HasExtension.val_map_lt_one_iff, one_le_val_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, ValuationSubring.valuation_eq_one_iff, Compatible.vle_iff_le, ValuativeRel.ValueGroupWithZero.lift_valuation, coe_mk, IsEquiv.lt_one_iff_lt_one, Int.padicValuation_le_one, isEquiv_iff_val_lt_one, WithVal.valuation_equiv_symm, NormedField.valuation_apply, IsUniformizer.val_lt_one, Valued.loc_const, mem_integer_iff, one_apply_def, WeierstrassCurve.IsGoodReduction.goodReduction, Valued.isClopen_closedBall, IsValuativeTopology.mem_nhds_iff, ValuationSubring.valuation_surjective, pos_iff, Valued.norm_pos_iff_valuation_pos, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, map_zero, Valued.toNormedField.norm_lt_one_iff, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq, Integers.one_of_isUnit, IsRankOneDiscrete.exists_generator_lt_one, AddValuation.ofValuation_apply, IsValuativeTopology.isOpen_sphere, FunctionField.inftyValuation_apply, ValuationSubring.mapOfLE_comp_valuation, val_le_one_iff, LaurentSeries.exists_ratFunc_eq_v, Valued.toNormedField.one_le_norm_iff, ValuativeRel.ValueGroupWithZero.mk_eq_valuation, coeff_zero_minpoly, map_add_supp, IsRankOneDiscrete.generator_mem_range, IsValuativeTopology.isClopen_closedBall, Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, IsDedekindDomain.HeightOneSpectrum.intValuation_apply, Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange, LaurentSeries.valuation_X_pow, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem, Int.padicValuation_eq_zero_iff, Integers.dvd_iff_le, one_rel_iff, le_one_of_subsingleton, Rat.padicValuation_le_one_iff, one_apply_eq_one_iff, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, Polynomial.valuation_X_eq_neg_one
leAddSubgroup 📖	CompOp	4 math math: mem_leAddSubgroup_iff, ltAddSubgroup_le_leAddSubgroup, leAddSubgroup_zero, leAddSubgroup_monotone
ltAddSubgroup 📖	CompOp	6 math math: Valued.toUniformSpace_eq, ltAddSubgroup_monotone, subgroups_basis, mem_ltAddSubgroup_iff, ltAddSubgroup_le_leAddSubgroup, coe_ltAddSubgroup
map 📖	CompOp	3 math math: IsEquiv.map, isEquiv_map_self_of_strictMono, map_apply
ofAddValuation 📖	CompOp	5 math math: ofAddValuation_apply, ofAddValuation_toAddValuation, toAddValuation_symm_eq, toValuation_ofValuation, ofAddValuation_symm_eq
one 📖	CompOp	10 math math: one_apply_lt_one_iff, one_apply_of_ne_zero, toMonoidWithZeroHom_one, one_apply_eq_zero_iff, one_apply_le_one, ValuativeRel.one_apply_posSubmonoid, ValuativeRel.trivialRel_eq_ofValuation_one, not_isNontrivial_one, one_apply_def, one_apply_eq_one_iff
supp 📖	CompOp	8 math math: supp_quot_supp, mem_supp_iff, ValuativeRel.supp_eq_valuation_supp, IsDedekindDomain.HeightOneSpectrum.valuation_def, comap_supp, instIsPrimeSuppOfNontrivialOfNoZeroDivisors, self_le_supp_comap, AddValuation.supp_quot_supp
toAddValuation 📖	CompOp	5 math math: toAddValuation_apply, ofAddValuation_toAddValuation, toAddValuation_symm_eq, toValuation_ofValuation, ofAddValuation_symm_eq
toMonoidWithZeroHom 📖	CompOp	4 math math: toFun_eq_coe, toMonoidWithZeroHom_one, map_add_le_max', toMonoidWithZeroHom_coe_eq_coe
toPreorder 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsNontrivial_iff_exists_one_lt 📖	mathematical	—	IsNontrivial DivisionRing.toRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation instFunLike	—	IsNontrivial.exists_one_lt GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass instValuationClass map_zero MonoidWithZeroHomClass.toZeroHomClass
coe_coe 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass
coe_ltAddSubgroup 📖	mathematical	—	SetLike.coe AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddSubgroup.instSetLike ltAddSubgroup setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation instFunLike Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—
coe_mk 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder ZeroHom.toFun MulZeroClass.toZero MulZeroOneClass.toMulZeroClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.toZeroHom Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemilatticeSup.toMax Lattice.toSemilatticeSup	DFunLike.coe Valuation instFunLike MonoidWithZeroHom MonoidWithZeroHom.funLike	—	—
comap_apply 📖	mathematical	—	DFunLike.coe Valuation instFunLike comap RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingHom.instFunLike	—	—
comap_comp 📖	mathematical	—	comap RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring	—	ext
comap_id 📖	mathematical	—	comap RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring	—	ext
comap_supp 📖	mathematical	—	supp comap CommRing.toRing Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.instRingHomClass	—	Ideal.ext RingHom.instRingHomClass mem_supp_iff Ideal.mem_comap comap_apply
ext 📖	—	DFunLike.coe Valuation instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe Valuation instFunLike	—	ext
instIsPrimeSuppOfNontrivialOfNoZeroDivisors 📖	mathematical	—	Ideal.IsPrime CommSemiring.toSemiring CommRing.toCommSemiring supp	—	one_ne_zero NeZero.one map_one mem_supp_iff Submodule.mem_top NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero map_mul
instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial 📖	mathematical	—	Nontrivial Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike Semiring.toMonoidWithZero Ring.toSemiring ValuationClass.toMonoidWithZeroHomClass instValuationClass	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass IsNontrivial.exists_val_nontrivial Subgroup.nontrivial_iff_exists_ne_one MonoidWithZeroHom.mem_valueGroup Set.mem_range_self
instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial 📖	mathematical	—	Nontrivial Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Submonoid Units.instMulOneClass SetLike.instMembership Submonoid.instSetLike MonoidWithZeroHom.valueMonoid Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike Semiring.toMonoidWithZero Ring.toSemiring ValuationClass.toMonoidWithZeroHomClass instValuationClass	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass IsNontrivial.exists_val_nontrivial Submonoid.nontrivial_iff_exists_ne_one MonoidWithZeroHom.mem_valueMonoid Set.mem_range_self
instValuationClass 📖	mathematical	—	ValuationClass Valuation instFunLike	—	MonoidWithZeroHom.map_mul' MonoidWithZeroHom.map_one' ZeroHom.map_zero' map_add_le_max'
isEquiv_iff_val_eq_one 📖	mathematical	—	IsEquiv DivisionRing.toRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	IsEquiv.eq_one_iff_eq_one isEquiv_of_val_le_one lt_or_eq_of_le map_one map_add_eq_of_lt_left map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass neg_add_cancel_left le_trans map_add map_neg max_self le_of_eq
isEquiv_iff_val_le_one 📖	mathematical	—	IsEquiv DivisionRing.toRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	IsEquiv.le_one_iff_le_one isEquiv_of_val_le_one
isEquiv_iff_val_lt_one 📖	mathematical	—	IsEquiv DivisionRing.toRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	IsEquiv.lt_one_iff_lt_one isEquiv_iff_val_eq_one zero_iff GroupWithZero.toNontrivial NeZero.one ne_iff_lt_or_gt Eq.not_lt map_inv₀ ValuationClass.toMonoidWithZeroHomClass instValuationClass inv_eq_iff_eq_inv inv_one one_lt_val_iff
isEquiv_iff_val_lt_val 📖	mathematical	—	IsEquiv DivisionRing.toRing Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	—	—
isEquiv_iff_val_sub_one_lt_one 📖	mathematical	—	IsEquiv DivisionRing.toRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	isEquiv_iff_val_lt_one Function.Surjective.forall Equiv.surjective
isEquiv_map_self_of_strictMono 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.funLike	IsEquiv map StrictMono.monotone	—	StrictMono.monotone StrictMono.le_iff_le
isEquiv_of_val_le_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	IsEquiv	—	eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass GroupWithZero.toNontrivial div_le_one₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono zero_lt_iff ne_zero_iff map_div
isEquiv_tfae 📖	mathematical	—	List.TFAE IsEquiv DivisionRing.toRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	—	isEquiv_iff_val_lt_val isEquiv_iff_val_le_one isEquiv_iff_val_eq_one isEquiv_iff_val_lt_one isEquiv_iff_val_sub_one_lt_one List.tfae_of_cycle
isNontrivial_iff_exists_lt_one 📖	mathematical	—	IsNontrivial DivisionRing.toRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	IsNontrivial.exists_lt_one GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass instValuationClass LT.lt.ne
isNontrivial_iff_exists_unit 📖	mathematical	—	IsNontrivial DivisionRing.toRing	—	ne_zero_iff Units.ne_zero DivisionRing.toNontrivial
isNontrivial_of_isEquiv 📖	mathematical	IsEquiv DivisionRing.toRing	IsNontrivial	—	IsEquiv.eq_zero IsEquiv.eq_one_iff_eq_one
leAddSubgroup_monotone 📖	mathematical	—	Monotone AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero AddSubgroup.instPartialOrder leAddSubgroup	—	LE.le.trans'
leAddSubgroup_zero 📖	mathematical	—	leAddSubgroup DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Bot.bot AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddSubgroup.instBot	—	AddSubgroup.ext GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass instValuationClass
le_one_of_subsingleton 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	map_one le_refl
ltAddSubgroup_le_leAddSubgroup 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder ltAddSubgroup leAddSubgroup Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	LT.lt.le
ltAddSubgroup_monotone 📖	mathematical	—	Monotone Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero AddSubgroup.instPartialOrder ltAddSubgroup	—	LE.le.trans_lt' Units.val_le_val
map_add 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemilatticeSup.toMax Lattice.toSemilatticeSup	—	map_add_le_max'
map_add' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	le_max_iff map_add
map_add_eq_of_lt_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	add_comm map_add_eq_of_lt_right
map_add_eq_of_lt_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	map_add_of_distinct_val LT.lt.ne max_eq_right_iff LT.lt.le
map_add_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	le_trans map_add max_le
map_add_le_max' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder ZeroHom.toFun MulZeroClass.toZero MulZeroOneClass.toMulZeroClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.toZeroHom toMonoidWithZeroHom Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
map_add_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	lt_of_le_of_lt map_add max_lt
map_add_of_distinct_val 📖	mathematical	—	DFunLike.coe Valuation instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder	—	lt_irrefl add_sub_cancel_right map_sub max_lt max_eq_left_of_lt add_comm max_comm Ne.lt_or_gt le_iff_eq_or_lt map_add
map_add_of_left_eq_zero 📖	mathematical	DFunLike.coe Valuation instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	sub_neg_eq_add map_sub_of_left_eq_zero map_neg
map_add_of_right_eq_zero 📖	mathematical	DFunLike.coe Valuation instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	add_comm map_add_of_left_eq_zero
map_add_supp 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule supp	DFunLike.coe Valuation CommRing.toRing instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	le_trans map_add max_le le_rfl le_antisymm add_neg_cancel_right Ideal.neg_mem_iff
map_apply 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.funLike	Valuation instFunLike map	—	—
map_div 📖	mathematical	—	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing instFunLike DivInvMonoid.toDiv DivisionRing.toDivInvMonoid GroupWithZero.toDivInvMonoid CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	map_div₀ ValuationClass.toMonoidWithZeroHomClass instValuationClass
map_eq_of_sub_lt 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	—	map_add_of_distinct_val ne_of_gt sub_add_cancel max_eq_right le_of_lt
map_inv 📖	mathematical	—	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing instFunLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	map_inv₀ ValuationClass.toMonoidWithZeroHomClass instValuationClass
map_mul 📖	mathematical	—	DFunLike.coe Valuation instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	MonoidWithZeroHom.map_mul'
map_neg 📖	mathematical	—	DFunLike.coe Valuation instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	MonoidHom.map_neg LinearOrderedCommMonoidWithZero.toIsMulTorsionFree
map_one 📖	mathematical	—	DFunLike.coe Valuation instFunLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	MonoidWithZeroHom.map_one'
map_one_add_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	map_one map_add_eq_of_lt_left
map_one_sub_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	sub_eq_add_neg map_one map_add_eq_of_lt_left map_neg
map_pow 📖	mathematical	—	DFunLike.coe Valuation instFunLike Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	MonoidHom.map_pow
map_sub 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sub_eq_add_neg map_add map_neg
map_sub_eq_of_lt_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sub_eq_add_neg map_add_eq_of_lt_left map_neg
map_sub_eq_of_lt_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sub_eq_add_neg map_add_eq_of_lt_right map_neg
map_sub_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sub_eq_add_neg map_add_le Eq.trans_le map_neg
map_sub_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sub_eq_add_neg map_add_lt Eq.trans_lt map_neg
map_sub_of_left_eq_zero 📖	mathematical	DFunLike.coe Valuation instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	max_self map_sub map_sub_eq_of_lt_right
map_sub_of_right_eq_zero 📖	mathematical	DFunLike.coe Valuation instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	map_sub_swap map_sub_of_left_eq_zero
map_sub_swap 📖	mathematical	—	DFunLike.coe Valuation instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	MonoidHom.map_sub_swap LinearOrderedCommMonoidWithZero.toIsMulTorsionFree
map_sum_eq_of_lt 📖	mathematical	Finset Finset.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	eq_or_ne Finset.sum_congr Finset.sum_const nsmul_eq_mul map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass MulZeroClass.mul_zero Finset.sum_eq_add_sum_diff_singleton map_add_eq_of_lt_left map_sum_lt
map_sum_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Finset.induction_on zero_le' map_zero Finset.sum_insert map_add_le Finset.forall_mem_insert
map_sum_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Finset.induction_on zero_lt_iff map_zero Finset.sum_insert map_add_lt Finset.forall_mem_insert
map_sum_lt' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero DFunLike.coe Valuation instFunLike	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	map_sum_lt ne_of_gt
map_zero 📖	mathematical	—	DFunLike.coe Valuation instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	ZeroHom.map_zero'
mem_leAddSubgroup_iff 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership AddSubgroup.instSetLike leAddSubgroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation instFunLike	—	—
mem_ltAddSubgroup_iff 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership AddSubgroup.instSetLike ltAddSubgroup Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation instFunLike Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—
mem_supp_iff 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule supp DFunLike.coe Valuation CommRing.toRing instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	—
ne_zero_iff 📖	—	—	—	—	map_ne_zero ValuationClass.toMonoidWithZeroHomClass instValuationClass
ne_zero_of_isUnit 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring	—	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass ne_zero_of_unit
ne_zero_of_unit 📖	—	—	—	—	Units.ne_zero DivisionRing.toNontrivial
not_isNontrivial_one 📖	mathematical	—	IsNontrivial Valuation one IsDomain.toNontrivial Ring.toSemiring IsDomain.to_noZeroDivisors	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass one_apply_of_ne_zero
ofAddValuation_apply 📖	mathematical	—	DFunLike.coe Valuation instFunLike Equiv AddValuation OrderDual Additive instLinearOrderedAddCommMonoidWithTopOrderDualAdditive EquivLike.toFunLike Equiv.instEquivLike ofAddValuation Additive.toMul OrderDual.ofDual AddValuation.instFunLike	—	—
ofAddValuation_symm_eq 📖	mathematical	—	Equiv.symm AddValuation OrderDual Additive instLinearOrderedAddCommMonoidWithTopOrderDualAdditive Valuation ofAddValuation toAddValuation	—	—
ofAddValuation_toAddValuation 📖	mathematical	—	DFunLike.coe Equiv AddValuation OrderDual Additive instLinearOrderedAddCommMonoidWithTopOrderDualAdditive Valuation EquivLike.toFunLike Equiv.instEquivLike ofAddValuation toAddValuation	—	—
one_apply_def 📖	mathematical	—	DFunLike.coe Valuation instFunLike one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	—
one_apply_eq_one_iff 📖	mathematical	—	DFunLike.coe Valuation instFunLike one MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	MonoidWithZeroHom.one_apply_eq_one_iff
one_apply_eq_zero_iff 📖	mathematical	—	DFunLike.coe Valuation instFunLike one MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	MonoidWithZeroHom.one_apply_eq_zero_iff
one_apply_le_one 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike one MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	one_apply_def
one_apply_lt_one_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike one MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	one_apply_def LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one
one_apply_of_ne_zero 📖	mathematical	—	DFunLike.coe Valuation instFunLike one MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	—
one_le_val_iff 📖	mathematical	—	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 instFunLike InvOneClass.toInv GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	map_inv₀ ValuationClass.toMonoidWithZeroHomClass instValuationClass inv_le_one₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono pos_iff GroupWithZero.toNontrivial
one_lt_val_iff 📖	mathematical	—	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 instFunLike InvOneClass.toInv GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	map_inv₀ ValuationClass.toMonoidWithZeroHomClass instValuationClass inv_lt_one₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono pos_iff GroupWithZero.toNontrivial
pos_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike	—	zero_lt_iff ne_zero_iff
toAddValuation_apply 📖	mathematical	—	DFunLike.coe AddValuation OrderDual Additive instLinearOrderedAddCommMonoidWithTopOrderDualAdditive AddValuation.instFunLike Equiv Valuation EquivLike.toFunLike Equiv.instEquivLike toAddValuation OrderDual.toDual Additive.ofMul instFunLike	—	—
toAddValuation_symm_eq 📖	mathematical	—	Equiv.symm Valuation AddValuation OrderDual Additive instLinearOrderedAddCommMonoidWithTopOrderDualAdditive toAddValuation ofAddValuation	—	—
toFun_eq_coe 📖	mathematical	—	ZeroHom.toFun MulZeroClass.toZero MulZeroOneClass.toMulZeroClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.toZeroHom toMonoidWithZeroHom DFunLike.coe Valuation instFunLike	—	—
toMonoidWithZeroHom_coe_eq_coe 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.funLike toMonoidWithZeroHom Valuation instFunLike	—	—
toMonoidWithZeroHom_one 📖	mathematical	—	toMonoidWithZeroHom Valuation one MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.one	—	—
toValuation_ofValuation 📖	mathematical	—	DFunLike.coe Equiv Valuation AddValuation OrderDual Additive instLinearOrderedAddCommMonoidWithTopOrderDualAdditive EquivLike.toFunLike Equiv.instEquivLike toAddValuation ofAddValuation	—	—
unit_map_eq 📖	mathematical	—	Units.val MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero DFunLike.coe MonoidHom Units Semiring.toMonoidWithZero Ring.toSemiring MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map MonoidHomClass.toMonoidHom Valuation MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZero.toMulZeroOneClass instFunLike MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass	—	MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass
val_eq_one_iff 📖	mathematical	—	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero InvOneClass.toInv GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	map_inv₀ ValuationClass.toMonoidWithZeroHomClass instValuationClass
val_le_one_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero InvOneClass.toInv GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	map_inv₀ ValuationClass.toMonoidWithZeroHomClass instValuationClass one_le_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono pos_iff GroupWithZero.toNontrivial
val_le_one_or_val_inv_le_one 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero InvOneClass.toInv GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass inv_zero one_le_val_iff
val_le_one_or_val_inv_lt_one 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero Preorder.toLT InvOneClass.toInv GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass inv_zero LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one GroupWithZero.toNontrivial one_lt_val_iff
val_lt_one_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero InvOneClass.toInv GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	map_inv₀ ValuationClass.toMonoidWithZeroHomClass instValuationClass one_lt_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono pos_iff GroupWithZero.toNontrivial
val_mrange_zero 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero SetLike.instMembership Submonoid.instSetLike MonoidHom.mrange NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring Valuation instFunLike MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass instCommMonoidWithZeroSubtypeMemSubmonoidMrange	—	MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass
zero_iff 📖	mathematical	—	DFunLike.coe Valuation DivisionRing.toRing instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	map_eq_zero ValuationClass.toMonoidWithZeroHomClass instValuationClass

Valuation.IsEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	Valuation.IsEquiv	Valuation.comap	—	—
eq_one_iff_eq_one 📖	mathematical	Valuation.IsEquiv	DFunLike.coe Valuation Valuation.instFunLike MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	Valuation.map_one val_eq map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
eq_zero 📖	mathematical	Valuation.IsEquiv	DFunLike.coe Valuation Valuation.instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	val_eq Valuation.map_zero
isNontrivial_iff 📖	mathematical	Valuation.IsEquiv DivisionRing.toRing	Valuation.IsNontrivial	—	Valuation.isNontrivial_of_isEquiv symm
le_one_iff_le_one 📖	mathematical	Valuation.IsEquiv	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation Valuation.instFunLike MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	Valuation.map_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
lt_iff_lt 📖	mathematical	Valuation.IsEquiv	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation Valuation.instFunLike	—	le_iff_le_iff_lt_iff_lt
lt_one_iff_lt_one 📖	mathematical	Valuation.IsEquiv	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation Valuation.instFunLike MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	Valuation.map_one lt_iff_lt map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
map 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.funLike Valuation.IsEquiv	Valuation.map	—	Monotone.strictMono_of_injective StrictMono.le_iff_le
ne_zero 📖	—	Valuation.IsEquiv	—	—	Iff.ne eq_zero
of_eq 📖	mathematical	—	Valuation.IsEquiv	—	refl
one_le_iff_one_le 📖	mathematical	Valuation.IsEquiv	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike	—	Valuation.map_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
one_lt_iff_one_lt 📖	mathematical	Valuation.IsEquiv	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike	—	Valuation.map_one lt_iff_lt map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
pos_iff 📖	mathematical	Valuation.IsEquiv	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike	—	zero_lt_iff Iff.ne eq_zero
refl 📖	mathematical	—	Valuation.IsEquiv	—	—
trans 📖	—	Valuation.IsEquiv	—	—	—
val_eq 📖	mathematical	Valuation.IsEquiv	DFunLike.coe Valuation Valuation.instFunLike	—	—
val_sub_one_lt_one_iff 📖	mathematical	Valuation.IsEquiv DivisionRing.toRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation Valuation.instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	Valuation.isEquiv_iff_val_sub_one_lt_one

Valuation.IsNontrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lt_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing Valuation.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	Valuation.isNontrivial_iff_exists_unit ne_iff_lt_or_gt DivisionRing.toNontrivial
exists_one_lt 📖	mathematical	—	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 Valuation.instFunLike	—	exists_lt_one map_inv₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass one_lt_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono zero_lt_iff GroupWithZero.toNontrivial
exists_val_nontrivial 📖	—	—	—	—	—
nontrivial_codomain 📖	mathematical	—	Nontrivial	—	exists_val_nontrivial

Valuation.IsTrivialOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_one 📖	mathematical	—	DFunLike.coe Valuation Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	—
valuation_algebraMap_le_one 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	—

ValuationClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add_le_max 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
toMonoidWithZeroHomClass 📖	mathematical	—	MonoidWithZeroHomClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	—

(root)

Definitions

Name	Category	Theorems
AddValuation 📖	CompOp	61 math math: IsDiscreteValuationRing.addVal_zero, AddValuation.map_sub_swap, AddValuation.map_pow, AddValuation.map_apply, AddValuation.top_iff, ArchimedeanClass.FiniteResidueField.mk_eq_zero, AddValuation.map_add', Padic.addValuation.apply, ArchimedeanClass.FiniteElement.val_add, AddValuation.map_add_of_distinct_val, AddValuation.toValuation_ofValuation, multiplicity_addValuation_apply, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, HahnSeries.addVal_le_of_coeff_ne_zero, ArchimedeanClass.FiniteElement.val_mul, IsDiscreteValuationRing.addVal_def', Irreducible.addVal_pow, Valuation.ofAddValuation_apply, IsDiscreteValuationRing.addVal_uniformizer, ArchimedeanClass.FiniteElement.val_sub, Valuation.toAddValuation_apply, AddValuation.map_zero, Valuation.ofAddValuation_toAddValuation, HahnSeries.addVal_apply_of_ne, IsDiscreteValuationRing.addVal_mul, IsDiscreteValuationRing.addVal_add, ArchimedeanClass.FiniteResidueField.mk_eq_mk, AddValuation.ofValuation_toValuation, AddValuation.map_mul, Valuation.toAddValuation_symm_eq, ArchimedeanClass.FiniteElement.val_zero, ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, IsDiscreteValuationRing.addVal_pow, ArchimedeanClass.FiniteResidueField.mk_ne_zero, AddValuation.map_neg, ArchimedeanClass.FiniteElement.val_one, IsDiscreteValuationRing.addVal_eq_zero_iff, AddValuation.of_apply, AddValuation.map_sub, AddValuation.map_add_supp, AddValuation.toValuation_apply, IsDiscreteValuationRing.addVal_eq_top_iff, IsDiscreteValuationRing.addVal_eq_zero_of_unit, IsDiscreteValuationRing.addVal_def, AddValuation.mem_supp_iff, AddValuation.map_div, IsDiscreteValuationRing.addVal_one, AddValuation.IsEquiv.val_eq, AddValuation.toValuation_symm_eq, IsDiscreteValuationRing.addVal_le_iff_dvd, Valuation.toValuation_ofValuation, AddValuation.ofValuation_symm_eq, AddValuation.map_add, AddValuation.map_one, ArchimedeanClass.addValuation_apply, HahnSeries.addVal_apply, AddValuation.ofValuation_apply, Valuation.ofAddValuation_symm_eq, ArchimedeanClass.FiniteElement.ext_iff, AddValuation.ext_iff, AddValuation.map_inv
ValuationClass 📖	CompData	1 math math: Valuation.instValuationClass
instCoeTCValuationOfValuationClass 📖	CompOp	—

---

← Back to Index