Basic

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

Statistics

Metric	Count
Definitions AddValuation, IsEquiv, comap, instFunLike, map, of, ofValuation, supp, toPreorder, toValuation, IsEquiv, orderMonoidIso, valueGroup₀Fun, IsNontrivial, IsTrivialOn, comap, instCommGroupWithZeroSubtypeMemSubmonoidMrange, instCommMonoidWithZeroSubtypeMemSubmonoidMrange, instFunLike, leAddSubgroup, ltAddSubgroup, map, ofAddValuation, one, restrict, supp, toAddValuation, toMonoidWithZeroHom, toPreorder, ValuationClass, instCoeTCValuationOfValuationClass	31
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_iff, eq_one_iff_eq_one, eq_zero, isNontrivial_iff, isTrivialOn, isTrivialOn_iff, le_iff_le, 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, orderMonoidIso_eq_refl, orderMonoidIso_spec, orderMonoidIso_symm, orderMonoidIso_trans, pos_iff, refl, restrict, trans, val_eq, val_sub_one_lt_one_iff, valueGroup₀Fun_spec, valueGroup₀Fun_zero, 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, embedding_restrict, exists_div_eq_of_unit, 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_restrict, 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, restrict_def, restrict_eq_mk, restrict_eq_one_iff, restrict_eq_zero_iff, restrict_inj, restrict_le_iff, restrict_le_iff_le_embedding, restrict_le_one_iff, restrict_lt_iff, restrict_lt_iff_lt_embedding, restrict_lt_one_iff, restrict_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	194
Total	225

AddValuation

Definitions

Name	Category	Theorems
IsEquiv 📖	MathDef	6 math math: IsEquiv.map, IsEquiv.of_eq, IsEquiv.comap, IsEquiv.refl, IsEquiv.symm, IsEquiv.trans
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	53 math math: IsDiscreteValuationRing.addVal_zero, map_sub_swap, map_pow, map_apply, top_iff, map_add', Padic.addValuation.apply, map_le_add, map_add_of_distinct_val, map_lt_sum, multiplicity_addValuation_apply, HahnSeries.addVal_le_of_coeff_ne_zero, map_eq_of_lt_sub, 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_add_eq_of_lt_left, map_mul, IsDiscreteValuationRing.addVal_pow, map_neg, map_lt_add, IsDiscreteValuationRing.addVal_eq_zero_iff, of_apply, map_sub, map_add_eq_of_lt_right, map_add_supp, map_sub_eq_of_lt_left, toValuation_apply, IsDiscreteValuationRing.addVal_eq_top_iff, map_le_sub, IsDiscreteValuationRing.addVal_eq_zero_of_unit, IsDiscreteValuationRing.addVal_def, mem_supp_iff, map_sub_eq_of_lt_right, map_div, IsDiscreteValuationRing.addVal_one, IsEquiv.val_eq, map_lt_sum', IsDiscreteValuationRing.addVal_le_iff_dvd, map_add, map_one, ArchimedeanClass.addValuation_apply, HahnSeries.addVal_apply, ofValuation_apply, ext_iff, map_inv, map_le_sum
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	5 math math: self_le_supp_comap, comap_supp, mem_supp_iff, supp_quot_supp, supp_quot
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	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	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	DFunLike.coe AddValuation instFunLike map AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearOrderedAddCommMonoidWithTop.toAddCommMonoid AddMonoidHom.instFunLike	—	—
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 📖	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	DFunLike.coe AddValuation instFunLike	—	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	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	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	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	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	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	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_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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring AddMonoid.toNSMul 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	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	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.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.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 📖	mathematical	AddValuation.IsEquiv	AddValuation.IsEquiv	—	Valuation.IsEquiv.trans
val_eq 📖	mathematical	AddValuation.IsEquiv	DFunLike.coe AddValuation AddValuation.instFunLike	—	Valuation.IsEquiv.eq_iff

Valuation

Definitions

Name	Category	Theorems
IsEquiv 📖	MathDef	27 math math: IsEquiv.map, isEquiv_iff_val_sub_one_lt_one, isEquiv_map_self_of_strictMono, isEquiv_valuation_valuationSubring, isEquiv_iff_val_lt_val, RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one, IsEquiv.restrict, RatFunc.adicValuation_not_isEquiv_infty_valuation, isEquiv_restrict, RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one, IsEquiv.trans, isEquiv_iff_val_le_one, isEquiv_iff_val_eq_one, isEquiv_of_val_le_one, RatFunc.valuation_isEquiv_infty_or_adic, ValuativeRel.isEquiv, HasExtension.val_isEquiv_comap, RatFunc.valuation_isEquiv_adic_of_not_isEquiv_infty, RatFunc.valuation_isEquiv_inftyValuation_of_one_lt_valuation_X, IsEquiv.symm, Rat.HeightOneSpectrum.valuation_equiv_padicValuation, isEquiv_tfae, isEquiv_iff_val_lt_one, IsEquiv.refl, IsEquiv.of_eq, IsEquiv.comap, isEquiv_iff_valuationSubring
IsNontrivial 📖	CompData	19 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, IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntIntValuation, RankOne.isNontrivial_restrict, valuationSubring_eq_top_iff, IsRankOneDiscrete.instIsNontrivial, isNontrivial_iff_not_a_field, isNontrivial_of_isEquiv
IsTrivialOn 📖	CompData	6 math math: IsEquiv.isTrivialOn_iff, FunctionField.instIsTrivialOnWithZeroMultiplicativeIntRatFuncInftyValuation, FiniteField.instIsTrivialOn, IsTrivialOn.of_le_one, FiniteField.instIsTrivialOn, IsEquiv.isTrivialOn
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	483 math math: mem_nhds_zero_iff, Valued.continuous_extension, Valued.isOpen_closedball, IsTrivialOn.valuation_algebraMap_le_one, Irreducible.maximalIdeal_eq_setOf_le_v_coe, inversion_estimate', WithVal.valued_toVal, ValuationSubring.valuation_lt_one_iff, leSubmodule_v_le_of_mem, FiniteField.algebraMap_le_one, FiniteField.algebraMap_eq_one, WithVal.valueGroupOrderIso₀_symm_apply, HasExtension.val_map_le_iff, isEquiv_iff_val_sub_one_lt_one, one_apply_lt_one_iff, isClopen_closedBall, mem_maximalIdeal_iff, val_mrange_zero, mem_leSubmodule_iff, map_one_add_of_lt, mem_supp_iff, Padic.withValUniformEquiv_norm_le_one_iff, Valued.toNormedField.norm_le_one_iff, Rat.padicValuation_cast, Valued.extension_extends, WithVal.valueGroup_eq, Valued.valuedCompletion_surjective_iff, ValuativeRel.valuation_eq_zero_iff, ValuationSubring.valuation_le_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff_mem_primeCompl, PadicComplex.valuation_extends, IsRankOneDiscrete.exists_generator_lt_one', WeierstrassCurve.HasAdditiveReduction.badReduction, RatFunc.exists_zpow_uniformizingPolynomial, IsTrivialOn.eq_one, Integers.one_of_isUnit', mem_ltIdeal_iff, toFun_eq_coe, val_le_one_or_val_inv_lt_one, NumberField.FinitePlace.norm_def', WithVal.valueGroupOrderIso₀_restrict, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, FunctionField.inftyValuation.X_inv, WithVal.apply_ofVal, IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, Int.padicValuation_lt_one_iff, map_add_eq_of_lt_right, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, IsRankOneDiscrete.generator_mem_valueGroup, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, WithVal.valueGroupOrderIso₀_apply, Integers.isPrincipal_iff_exists_isGreatest, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, LaurentSeries.valuation_single_zpow, RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero, Valued.toUniformSpace_eq, IsDedekindDomain.HeightOneSpectrum.intValuation_le_one, ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl, instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial, WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral, ValuationSubring.valuation_unit, NumberField.HeightOneSpectrum.rankOne_hom'_def, Compatible.srel_iff_lt, WithVal.valueGroupEquiv_symm_apply, IsEquiv.valuedCompletion_le_one_iff, isEquiv_iff_val_lt_val, restrict_eq_one_iff, IsRankOneDiscrete.generator'_lt_one, 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, IsEquiv.restrict, ext_iff, Rat.padicValuation_self, ltIdeal_v_le_of_mem, Valued.isClopen_ball, ValuativeRel.ValueGroupWithZero.embed_strictMono, IsEquiv.pos_iff, Valued.exists_coe_eq_v, ValuativeRel.ValueGroupWithZero.mk_eq_div, unit_map_eq, Integers.le_of_dvd, hasBasis_nhds_zero, Polynomial.valuation_of_mk, WeierstrassCurve.hasGoodReduction_iff, val_lt_one_iff, IsUniformizer.zpowers_eq_valueGroup, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀, val_le_one_or_val_inv_le_one, map_add_of_distinct_val, restrict_le_iff, IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono, map_add, HasExtension.val_map_lt_iff, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, map_div, restrict_eq_zero_iff, one_lt_val_iff, WeierstrassCurve.hasMultiplicativeReduction_iff, Padic.norm_eq_zpow_log_mulValuation, restrict_eq_mk, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, 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, restrict_lt_iff_lt_embedding, LaurentSeries.val_le_one_iff_eq_coe, NumberField.HeightOneSpectrum.adicAbv_def, Valued.extension_eq_zero_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer, WithVal.val_apply_equiv, IsValuativeTopology.isClopen_sphere, FunctionField.valuedFqtInfty.def, coe_coe, subgroups_basis, WithVal.apply_equiv, IsEquiv.one_lt_iff_one_lt, map_sub_eq_of_lt_right, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, map_add_le, mem_unitGroup_iff, Valued.isOpen_sphere, restrict_le_iff_le_embedding, IsDedekindDomain.HeightOneSpectrum.valuation_def, ValuationSubring.valuation_le_one, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, isEquiv_restrict, nonempty_rankOne_iff_mulArchimedean, LaurentSeries.exists_ratFunc_val_lt, RankOne.exists_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', WeierstrassCurve.HasGoodReduction.goodReduction, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd, WithVal.strictMono_valueGroupOrderIso₀, map_sub_swap, isEquiv_iff_val_le_one, WithVal.strictMono_valueGroupOrderIso₀_symm, 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, RatFunc.valuation_surjective, ofAddValuation_apply, Integers.isIntegral_iff_v_le_one, ValuativeExtension.mapValueGroupWithZero_valuation, isEquiv_iff_val_eq_one, WithVal.valueGroupEquiv_apply, Integers.isPrincipalIdealRing_iff_not_denselyOrdered, Polynomial.valuation_inv_monomial_eq_valuation_X_zpow, RankOne.strictMono, Integers.le_iff_dvd, LaurentSeries.exists_Polynomial_intValuation_lt, ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀, ValuationSubring.valuation_le_one_iff, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, ValuationSubring.mem_unitGroup_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk, toAddValuation_apply, Valued.isClosed_ball, zero_iff, restrict_lt_one_iff, map_sub_le, srel_iff_lt, Valued.isClopen_sphere, PadicAlgCl.valuation_p, PadicComplex.valuation_p, Valued.isClosed_sphere, IsValuativeTopology.isClosed_closedBall, FiniteField.valuation_algebraMap_eq_one, Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, one_apply_eq_zero_iff, IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', WithVal.lt_def, cauchy_iff, locally_const, 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, IsRankOneDiscrete.embedding_generator', Valued.locally_const, mem_leAddSubgroup_iff, vle_iff_le, ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, Valued.toNormedField.norm_le_iff, map_add', IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, restrict_inj, map_sum_lt, map_add_lt, Valued.integer.mulArchimedean_mrange_of_isCompact_integer, Integers.dvdNotUnit_iff_lt, Padic.valuation_p_lt_one, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, embedding_restrict, Integers.valuation_unit, IsEquiv.lt_iff_lt, map_mul, map_sum_lt', 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, Polynomial.valuation_le_one_of_valuation_X_le_one, ValuationSubring.valuation_eq_iff, ValuativeRel.one_apply_posSubmonoid, instValuationClass, comap_apply, map_add_eq_of_lt_left, map_one_sub_of_lt, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, NumberField.FinitePlace.norm_def_int, leIdeal_v_le_of_mem, veq_iff_eq, IsValuativeTopology.hasBasis_nhds_zero', extendToLocalization_mk', WeierstrassCurve.hasAdditiveReduction_iff, IsRankOneDiscrete.generator'_zpowers_eq_top, Integers.maximalIdeal_eq_setOf_le_v_algebraMap, WeierstrassCurve.HasAdditiveReduction.additiveReduction, map_one, restrict_pos_iff, one_vlt_iff, IsValuativeTopology.isClopen_ball, IsValuativeTopology.hasBasis_nhds, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd, one_vle_iff, restrict_def, 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, IsEquiv.orderMonoidIso_trans, WithVal.strictMono_valueGroupEquiv_symm, mem_ltAddSubgroup_iff, IsRankOneDiscrete.generator_zpowers_eq_valueGroup, LaurentSeries.valuation_LaurentSeries_equal_extension, isClosed_closedBall, 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, toTopologicalSpace_eq, map_sub_eq_of_lt_left, ValuativeRel.exists_valuation_div_valuation_eq, map_apply, IsNontrivial.exists_one_lt, IsDedekindDomain.HeightOneSpectrum.intValuation_def, PadicAlgCl.valuation_def, FunctionField.inftyValuation.X, Polynomial.valuation_monomial_eq_valuation_X_pow, toMonoidWithZeroHom_coe_eq_coe, map_sum_eq_of_lt, srel_one_iff, RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty, PadicAlgCl.valuation_coe, IsUniformizer.val_pos, isClopen_ball, FunctionField.inftyValuedFqt.def, vle_one_iff, IsEquiv.val_sub_one_lt_one_iff, Integers.coe_span_singleton_eq_setOf_le_v_algebraMap, IsEquiv.eq_iff, IsValuativeTopology.hasBasis_nhds', Integers.valuation_pos_iff_ne_zero, Valued.isOpen_closedBall, instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial, hasBasis_nhds, RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X, IsEquiv.one_le_iff_one_le, ltSubmodule_v_le_of_mem, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, Valued.mem_nhds_zero, RankLeOne.exists_val_lt, HasExtension.val_map_eq_one_iff, Valued.isOpen_ball, ValuationSubring.mem_principalUnitGroup_iff, NormedField.v_eq_valuation, Valued.mem_nhds, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq, IsEquiv.le_iff_le, map_neg, Polynomial.valuation_aeval_monomial_eq_valuation_pow, isOpen_ball, 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_surjective, 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, PadicComplex.RankOne.hom_eq_embedding, WithVal.valueGroupOrderIso₀_symm_restrict, vlt_one_iff, map_eq_one_of_forall_lt, LaurentSeries.valuation_compare, IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, map_add_of_left_eq_zero, hasBasis_uniformity, Valued.toNormedField.norm_def, LaurentSeries.tendsto_valuation, toUniformSpace_eq, isOpen_sphere, IsEquiv.le_one_iff_le_one, integer.coe_span_singleton_eq_setOf_le_v_coe, norm_def, Integers.wellFounded_gt_on_v_iff_discrete_mrange, map_sub_of_right_eq_zero, PowerSeries.intValuation_X, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', exists_div_eq_of_unit, restrict_le_one_iff, isClosed_ball, map_eq_of_sub_lt, IsEquiv.val_eq, IsEquiv.orderMonoidIso_eq_refl, HasExtension.mk_smul_mk, ValuationSubring.mem_nonunits_iff, Valued.toNormedField.norm_lt_iff, map_pow, rel_iff_le, RankOne.zero_of_hom_zero, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, IsEquiv.valueGroup₀Fun_zero, IsEquiv.valueGroup₀Fun_spec, Integers.valuation_irreducible_pos, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, vlt_iff_lt, IsUniformizer.iff, Valued.hasBasis_uniformity, mem_ltSubmodule_iff, ModP.v_p_lt_val, ValuativeRel.valuation_lt_symm_orderMonoidIso, 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, FiniteField.valuation_algebraMap_le_one, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, restrict_lt_iff, extendToLocalization_apply_map_apply, IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply, mem_leIdeal_iff, Padic.norm_rat_le_one_iff_padicValuation_le_one, Valued.isClosed_closedBall, Set.integer_valuation_le_one, isOpen_closedBall, PreTilt.map_eq_zero, coe_ltAddSubgroup, Rat.surjective_padicValuation, RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one, RankOne.isNontrivial_restrict, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq, IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer, WithVal.le_def, RatFunc.valuation_uniformizingPolynomial_lt_one, HasExtension.val_map_lt_one_iff, ValuativeRel.restrict_lt_orderMonoidIso, one_le_val_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, ValuationSubring.valuation_eq_one_iff, Compatible.vle_iff_le, norm_pos_iff_valuation_pos, map_sub_lt, ValuativeRel.ValueGroupWithZero.lift_valuation, coe_mk, map_sum_le, IsEquiv.lt_one_iff_lt_one, Valued.continuous_valuation_of_surjective, Int.padicValuation_le_one, isEquiv_iff_val_lt_one, WithVal.valuation_equiv_symm, NormedField.valuation_apply, IsUniformizer.val_lt_one, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, NumberField.FinitePlace.norm_embedding', restrict_exists_div_eq, WeierstrassCurve.HasMultiplicativeReduction.badReduction, mem_integer_iff, one_apply_def, IsEquiv.orderMonoidIso_spec, RankOne.hom_eq_zero_iff, Valued.isClopen_closedBall, RankOne.restrict_RankOne_hom_eq, WithVal.strictMono_valueGroupEquiv, IsValuativeTopology.mem_nhds_iff, ValuationSubring.valuation_surjective, pos_iff, IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zero, Valued.exists_pow_lt_of_le_exp_neg_one, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, map_zero, RankLeOne.strictMono', Valued.toNormedField.norm_lt_one_iff, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq, exists_setOf_restrict_le_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono, Integers.one_of_isUnit, IsRankOneDiscrete.exists_generator_lt_one, AddValuation.ofValuation_apply, IsValuativeTopology.isOpen_sphere, FunctionField.inftyValuation_apply, ValuationSubring.mapOfLE_comp_valuation, IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zpow, val_le_one_iff, NumberField.FinitePlace.norm_embedding_int, LaurentSeries.exists_ratFunc_eq_v, Valued.toNormedField.one_le_norm_iff, map_sub_of_left_eq_zero, ValuativeRel.ValueGroupWithZero.mk_eq_valuation, coeff_zero_minpoly, map_add_supp, IsRankOneDiscrete.generator_mem_range, IsValuativeTopology.isClopen_closedBall, exists_div_eq_of_surjective, Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, IsDedekindDomain.HeightOneSpectrum.intValuation_apply, mem_nhds_iff, 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, NumberField.FinitePlace.norm_def, is_topological_valuation, one_rel_iff, le_one_of_subsingleton, inversion_estimate, isClopen_sphere, WeierstrassCurve.HasMultiplicativeReduction.multiplicativeReduction, IsEquiv.orderMonoidIso_symm, isClosed_sphere, map_add_of_right_eq_zero, Rat.padicValuation_le_one_iff, one_apply_eq_one_iff, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, Polynomial.valuation_X_eq_neg_one, Valued.extensionValuation_toFun
leAddSubgroup 📖	CompOp	4 math math: mem_leAddSubgroup_iff, ltAddSubgroup_le_leAddSubgroup, leAddSubgroup_zero, leAddSubgroup_monotone
ltAddSubgroup 📖	CompOp	8 math math: Valued.toUniformSpace_eq, ltAddSubgroup_monotone, subgroups_basis, mem_ltAddSubgroup_iff, toTopologicalSpace_eq, ltAddSubgroup_le_leAddSubgroup, toUniformSpace_eq, 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
restrict 📖	CompOp	74 math math: mem_nhds_zero_iff, Valued.isOpen_closedball, isClopen_closedBall, Valued.extension_extends, WithVal.valueGroupOrderIso₀_restrict, IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, restrict_eq_one_iff, IsEquiv.restrict, Valued.isClopen_ball, hasBasis_nhds_zero, restrict_le_iff, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, restrict_eq_zero_iff, restrict_eq_mk, Valued.continuous_valuation, restrict_lt_iff_lt_embedding, IsValuativeTopology.isClopen_sphere, Valued.isOpen_sphere, restrict_le_iff_le_embedding, isEquiv_restrict, RankOne.exists_val_lt, Valued.hasBasis_nhds_zero, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, Valued.isClosed_ball, restrict_lt_one_iff, Valued.isClopen_sphere, Valued.isClosed_sphere, IsValuativeTopology.isClosed_closedBall, cauchy_iff, restrict_inj, embedding_restrict, Valued.valuation_isClosedMap, Valued.cauchy_iff, restrict_pos_iff, IsValuativeTopology.isClopen_ball, restrict_def, isClosed_closedBall, IsValuativeTopology.isOpen_closedBall, isClopen_ball, Valued.isOpen_closedBall, hasBasis_nhds, Valued.mem_nhds_zero, RankLeOne.exists_val_lt, Valued.isOpen_ball, Valued.mem_nhds, isOpen_ball, IsValuativeTopology.isClosed_ball, WithVal.valueGroupOrderIso₀_symm_restrict, hasBasis_uniformity, Valued.toNormedField.norm_def, isOpen_sphere, norm_def, exists_div_eq_of_unit, restrict_le_one_iff, isClosed_ball, Valued.hasBasis_uniformity, ValuativeRel.valuation_lt_symm_orderMonoidIso, restrict_lt_iff, Valued.isClosed_closedBall, isOpen_closedBall, RankOne.isNontrivial_restrict, ValuativeRel.restrict_lt_orderMonoidIso, restrict_exists_div_eq, IsEquiv.orderMonoidIso_spec, Valued.isClopen_closedBall, RankOne.restrict_RankOne_hom_eq, exists_setOf_restrict_le_iff, IsValuativeTopology.isOpen_sphere, IsValuativeTopology.isClopen_closedBall, mem_nhds_iff, is_topological_valuation, isClopen_sphere, isClosed_sphere
supp 📖	CompOp	9 math math: supp_quot_supp, mem_supp_iff, ValuativeRel.supp_eq_valuation_supp, IsDedekindDomain.HeightOneSpectrum.valuation_def, comap_supp, supp_quot, 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 NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero 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
embedding_restrict 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.ValueGroup₀.embedding MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass
exists_div_eq_of_unit 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation instFunLike MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass WithZero.div Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subgroup.div MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict Units.val WithZero.instMonoidWithZero DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass Units.ne_zero WithZero.instNontrivial One.instNonempty MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.mem_valueGroup_iff_of_comm restrict_pos_iff restrict_def WithZero.pos_iff_ne_zero MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff GroupWithZero.noZeroDivisors GroupWithZero.toNontrivial zero_lt_iff div_eq_iff SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass mul_comm StrictMono.injective MonoidWithZeroHom.ValueGroup₀.embedding_strictMono map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass embedding_restrict WithZero.coe_unzero
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 instReflLe 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 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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder PartialOrder.toPreorder DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.funLike	—	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 DivisionRing.toRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	—	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_restrict 📖	mathematical	—	IsEquiv MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass instReflLe
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 Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring	—	ne_zero_iff Units.ne_zero DivisionRing.toNontrivial
isNontrivial_of_isEquiv 📖	mathematical	IsEquiv	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	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	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	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	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	DFunLike.coe Valuation instFunLike 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	DFunLike.coe Valuation instFunLike 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	DFunLike.coe Valuation instFunLike map MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MonoidWithZeroHom.funLike	—	—
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 📖	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	DFunLike.coe Valuation instFunLike	—	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	DFunLike.coe Valuation instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	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	DFunLike.coe Valuation instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	sub_eq_add_neg map_one map_add_eq_of_lt_left map_neg
map_pow 📖	mathematical	—	DFunLike.coe Valuation instFunLike Monoid.toPow 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	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	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	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	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	DFunLike.coe Valuation instFunLike 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	DFunLike.coe Valuation instFunLike 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 SetLike.instMembership Finset.instSetLike Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation instFunLike	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_of_mem 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	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	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	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	—	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 instReflLe
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
restrict_def 📖	mathematical	—	DFunLike.coe Valuation MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.ValueGroup₀.restrict₀	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass
restrict_eq_mk 📖	mathematical	—	DFunLike.coe Valuation MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict WithZero.coe Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass inv_one one_mul
restrict_eq_one_iff 📖	mathematical	—	DFunLike.coe Valuation MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict WithZero.one Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subgroup.one InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass restrict_def MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_one_iff
restrict_eq_zero_iff 📖	mathematical	—	DFunLike.coe Valuation MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict WithZero.instZero Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass restrict_def MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff
restrict_inj 📖	mathematical	—	DFunLike.coe Valuation MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass
restrict_le_iff 📖	mathematical	—	MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLE 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 DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass instReflLe
restrict_le_iff_le_embedding 📖	mathematical	—	MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLE 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 DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict WithZero.instMulZeroOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.ValueGroup₀.embedding	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ StrictMono.le_iff_le MonoidWithZeroHom.ValueGroup₀.embedding_strictMono restrict_def
restrict_le_one_iff 📖	mathematical	—	MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLE 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 DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict WithZero.one Subgroup.one InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass restrict_le_iff_le_embedding map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
restrict_lt_iff 📖	mathematical	—	MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT 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 DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass zero_lt_iff
restrict_lt_iff_lt_embedding 📖	mathematical	—	MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT 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 DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict WithZero.instMulZeroOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.ValueGroup₀.embedding	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ StrictMono.lt_iff_lt MonoidWithZeroHom.ValueGroup₀.embedding_strictMono restrict_def
restrict_lt_one_iff 📖	mathematical	—	MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT 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 DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict WithZero.one Subgroup.one InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass restrict_lt_iff_lt_embedding map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
restrict_pos_iff 📖	mathematical	—	MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT 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 WithZero.instZero DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass zero_lt_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

Definitions

Name	Category	Theorems
orderMonoidIso 📖	CompOp	5 math math: ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, orderMonoidIso_trans, orderMonoidIso_eq_refl, orderMonoidIso_spec, orderMonoidIso_symm
valueGroup₀Fun 📖	CompOp	2 math math: valueGroup₀Fun_zero, valueGroup₀Fun_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	Valuation.IsEquiv	Valuation.IsEquiv Valuation.comap	—	—
eq_iff 📖	mathematical	Valuation.IsEquiv	DFunLike.coe Valuation Valuation.instFunLike	—	—
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 eq_iff 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	—	eq_iff Valuation.map_zero
isNontrivial_iff 📖	mathematical	Valuation.IsEquiv	Valuation.IsNontrivial	—	Valuation.isNontrivial_of_isEquiv symm
isTrivialOn 📖	mathematical	Valuation.IsEquiv	Valuation.IsTrivialOn	—	eq_one_iff_eq_one Valuation.IsTrivialOn.eq_one
isTrivialOn_iff 📖	mathematical	Valuation.IsEquiv	Valuation.IsTrivialOn	—	isTrivialOn symm
le_iff_le 📖	mathematical	Valuation.IsEquiv	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation Valuation.instFunLike	—	—
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.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
orderMonoidIso_eq_refl 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	orderMonoidIso OrderMonoidIso.refl MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass 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 MulZeroClass.toMul WithZero.instMulZeroClass Subgroup.mul	—	OrderMonoidIso.ext ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass map_zero MonoidWithZeroHomClass.toZeroHomClass MulEquivClass.toMonoidWithZeroHomClass OrderMonoidIso.instMulEquivClass Iff.ne eq_zero valueGroup₀Fun_spec
orderMonoidIso_spec 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	DFunLike.coe OrderMonoidIso MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass 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 MulZeroClass.toMul WithZero.instMulZeroClass Subgroup.mul EquivLike.toFunLike OrderMonoidIso.instEquivLike orderMonoidIso MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass restrict Valuation.restrict_def MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff map_zero MonoidWithZeroHomClass.toZeroHomClass MulEquivClass.toMonoidWithZeroHomClass OrderMonoidIso.instMulEquivClass eq_zero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass NeZero.one GroupWithZero.toNontrivial Iff.ne symm valueGroup₀Fun_spec
orderMonoidIso_symm 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	OrderMonoidIso.symm MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass 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 MulZeroClass.toMul WithZero.instMulZeroClass Subgroup.mul orderMonoidIso	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
orderMonoidIso_trans 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	OrderMonoidIso.trans MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass 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 MulZeroClass.toMul WithZero.instMulZeroClass Subgroup.mul orderMonoidIso trans	—	OrderMonoidIso.ext ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass trans map_zero MonoidWithZeroHomClass.toZeroHomClass MulEquivClass.toMonoidWithZeroHomClass OrderMonoidIso.instMulEquivClass Iff.ne eq_zero valueGroup₀Fun_spec
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	—	—
restrict 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	Valuation.IsEquiv 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
trans 📖	mathematical	Valuation.IsEquiv	Valuation.IsEquiv	—	—
val_eq 📖	mathematical	Valuation.IsEquiv	DFunLike.coe Valuation Valuation.instFunLike	—	eq_iff
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 LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing 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
valueGroup₀Fun_spec 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	valueGroup₀Fun WithZero.coe Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass DFunLike.coe MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero Iff.ne eq_zero	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Iff.ne eq_zero valueGroup₀Fun.eq_1 eq_iff
valueGroup₀Fun_zero 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	valueGroup₀Fun 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

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	72 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, AddValuation.map_le_add, ArchimedeanClass.FiniteElement.val_add, AddValuation.map_add_of_distinct_val, AddValuation.map_lt_sum, AddValuation.toValuation_ofValuation, multiplicity_addValuation_apply, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, HahnSeries.addVal_le_of_coeff_ne_zero, AddValuation.map_eq_of_lt_sub, 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, AddValuation.map_add_eq_of_lt_left, 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, AddValuation.map_lt_add, ArchimedeanClass.FiniteElement.val_one, IsDiscreteValuationRing.addVal_eq_zero_iff, AddValuation.of_apply, AddValuation.map_sub, AddValuation.map_add_eq_of_lt_right, AddValuation.map_add_supp, AddValuation.map_sub_eq_of_lt_left, AddValuation.toValuation_apply, IsDiscreteValuationRing.addVal_eq_top_iff, AddValuation.map_le_sub, IsDiscreteValuationRing.addVal_eq_zero_of_unit, IsDiscreteValuationRing.addVal_def, AddValuation.mem_supp_iff, AddValuation.map_sub_eq_of_lt_right, AddValuation.map_div, IsDiscreteValuationRing.addVal_one, AddValuation.IsEquiv.val_eq, AddValuation.map_lt_sum', 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, AddValuation.map_le_sum
ValuationClass 📖	CompData	1 math math: Valuation.instValuationClass
instCoeTCValuationOfValuationClass 📖	CompOp	—

---

← Back to Index