Canonical

📁 Source: Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

Statistics

Metric	Count
Definitions linearOrderedCommMonoidWithZero, LinearOrderedCommGroupWithZero, toCommGroupWithZero, toDiv, toInv, toLinearOrderedCommMonoidWithZero, zpow, LinearOrderedCommMonoidWithZero, toCommMonoidWithZero, toLinearOrder, toOrderBot, decidableEq, decidableLE, decidableLT, expOrderIso, instBot, instBoundedOrder, instLT, instLattice, instLinearOrder, instLinearOrderedCommGroupWithZero, instLinearOrderedCommMonoidWithZero, instOrderBot, instPartialOrder, instPreorder, le, logOrderIso, semilatticeInf, semilatticeSup, instLinearOrderedAddCommGroupWithTopAdditiveOrderDual, instLinearOrderedAddCommGroupWithTopOrderDualAdditive, instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual, instLinearOrderedAddCommMonoidWithTopOrderDualAdditive, instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop, instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual	35
Theorems withZero, div_eq_mul_inv, inv_zero, mul_inv_cancel, toNontrivial, zpow_neg', zpow_succ', zpow_zero', toIsMulTorsionFree, toIsOrderedMonoid, toMulPosStrictMono, toPosMulStrictMono, toZeroLeOneClass, zero_le, zero_lt, addLeftMono, coe_inf, coe_le_coe, coe_le_iff, coe_le_one, coe_lt_coe, coe_lt_one, coe_sup, exists_ne_zero_and_le_and_le, exists_ne_zero_and_lt, exists_ne_zero_and_lt_and_lt, expOrderIso_symm_apply, exp_le_exp, exp_lt_exp, exp_pos, instCanonicallyOrderedAdd, instExistsAddOfLE, instMulLeftMono, instMulLeftReflectLT, isOrderedAddMonoid, isOrderedMonoid, le_coe_iff, le_def, le_exp_log, le_exp_of_log_le, le_log_iff_exp_le, le_log_of_exp_le, le_max_iff, le_ofAdd_iff, le_ofAdd_of_toAdd_unzero_le, le_unzero_iff, logOrderIso_apply, log_le_iff_le_exp, log_le_log, log_lt_iff_lt_exp, log_lt_log, lt_coe_iff, lt_def, lt_exp_of_log_lt, lt_iff_exists, lt_iff_exists_coe, lt_log_iff_exp_lt, lt_log_of_exp_lt, lt_mul_exp_iff_le, lt_ofAdd_iff, lt_ofAdd_of_toAdd_unzero_lt, lt_unzero_iff, map'_mono, map'_strictMono, min_le_iff, nonpos_iff_eq_zero, not_coe_le_zero, not_lt_zero, one_le_coe, one_lt_coe, pos_iff_ne_zero, toAdd_unzero_le_of_lt_ofAdd, toAdd_unzero_lt_of_lt_ofAdd, total_le, unbot_le_iff, unzero_le_unzero, unzero_lt_iff, val_expOrderIso_apply, val_inv_expOrderIso_apply, val_inv_logOrderIso_symm_apply, val_logOrderIso_symm_apply, zero_eq_bot, zero_le, zero_lt_coe, bot_eq_zero'', denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units, denselyOrdered_units_iff, instDenselyOrderedUnits, instIsCancelMulZero_1, instNontrivialUnitsOfDenselyOrdered, inv_mul_lt_of_lt_mul₀, le_zero_iff, lt_of_mul_lt_mul_of_le₀, mul_inv_lt_of_lt_mul₀, ne_zero_of_lt, not_lt_zero', ofAdd_bot, ofAdd_toDual_eq_zero_iff, ofDual_toAdd_eq_top_iff, ofDual_toAdd_zero, pow_pos_iff, zero_le', zero_lt_iff	103
Total	138

Function.Injective

Definitions

Name	Category	Theorems
linearOrderedCommMonoidWithZero 📖	CompOp	—

IsMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withZero 📖	mathematical	IsMax	IsMax WithZero WithZero.le WithZero.coe	—	withBot

LinearOrderedCommGroupWithZero

Definitions

Name	Category	Theorems
toCommGroupWithZero 📖	CompOp	298 math math: Valuation.mem_nhds_zero_iff, Valued.continuous_extension, Valuation.IsRankOneDiscrete.generator_lt_one, Valued.isOpen_closedball, Valuation.inversion_estimate', ValuationSubring.valuation_lt_one_iff, WithVal.valueGroupOrderIso₀_symm_apply, Valuation.ltIdeal_le_leIdeal, Valuation.isEquiv_iff_val_sub_one_lt_one, Valuation.isClopen_closedBall, Valuation.mem_maximalIdeal_iff, Valued.toNormedField.norm_le_one_iff, Valued.extension_extends, WithVal.valueGroup_eq, Valuation.IsRankOneDiscrete.exists_generator_lt_one', NNReal.exists_lt_of_strictMono, RatFunc.exists_zpow_uniformizingPolynomial, Valuation.Integers.one_of_isUnit', WithZeroTopology.nhds_zero, Valuation.mem_ltIdeal_iff, Valuation.val_le_one_or_val_inv_lt_one, WithVal.valueGroupOrderIso₀_restrict, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, Valuation.IsRankOneDiscrete.generator_mem_valueGroup, MonoidWithZeroHom.ValueGroup₀.monoidWithZeroHom_strictMono, WithVal.valueGroupOrderIso₀_apply, inl_mul_inr_eq_coe_toLex, RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero, Valued.toUniformSpace_eq, ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl, Valuation.instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial, ValuationSubring.valuation_unit, NumberField.HeightOneSpectrum.rankOne_hom'_def, WithVal.valueGroupEquiv_symm_apply, Valuation.IsEquiv.valuedCompletion_le_one_iff, Valuation.restrict_eq_one_iff, Valuation.IsRankOneDiscrete.generator'_lt_one, Valuation.isNontrivial_iff_exists_lt_one, Valuation.Integers.valuation_irreducible_lt_one, WithZeroTopology.nhds_zero_of_units, ValuationSubring.mapOfLE_valuation_apply, Valuation.Integers.map_le_one, MonoidWithZeroHom.fst_mono, Valuation.IsEquiv.restrict, Valuation.ltAddSubgroup_monotone, Valuation.ltIdeal_v_le_of_mem, Valued.isClopen_ball, ValuativeRel.ValueGroupWithZero.embed_strictMono, ValuativeRel.subsingleton_units_valueGroupWithZero_of_trivialRel, ValuativeRel.ValueGroupWithZero.mk_eq_div, Valuation.hasBasis_nhds_zero, ValuativeExtension.mapValueGroupWithZero_mk, Valuation.leIdeal_map_algebraMap_eq_leSubmodule_min, Valuation.val_lt_one_iff, Valuation.IsUniformizer.zpowers_eq_valueGroup, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀, Valuation.val_le_one_or_val_inv_le_one, Valuation.restrict_le_iff, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, Valuation.map_div, Valuation.restrict_eq_zero_iff, Valuation.one_lt_val_iff, Valuation.restrict_eq_mk, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, ValuationSubring.valuation_lt_one_or_eq_one, Valued.continuous_valuation, Valuation.val_eq_one_iff, Valuation.restrict_lt_iff_lt_embedding, Valued.extension_eq_zero_iff, MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos, ValuativeExtension.mapValueGroupWithZero_strictMono, IsValuativeTopology.isClopen_sphere, OrderMonoidIso.withZeroUnits_symm_apply, MonoidWithZeroHom.inl_strictMono, Valuation.subgroups_basis, OrderMonoidIso.withZeroUnits_apply, Valuation.mem_unitGroup_iff, Valued.isOpen_sphere, Valuation.restrict_le_iff_le_embedding, ValuationSubring.valuation_le_one, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, denselyOrdered_units_iff, OrderIso.withZeroUnits_symm_apply, Valuation.isEquiv_restrict, Valuation.nonempty_rankOne_iff_mulArchimedean, Valuation.RankOne.exists_val_lt, Valued.hasBasis_nhds_zero, Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup, IsValuativeTopology.mem_nhds_iff', mul_inv_lt_of_lt_mul₀, WithZero.withZeroUnitsEquiv_symm_strictMono, instNontrivialUnitsOfDenselyOrdered, WithVal.strictMono_valueGroupOrderIso₀, Valuation.isEquiv_iff_val_le_one, WithVal.strictMono_valueGroupOrderIso₀_symm, Valuation.IsUniformizer.val, ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq, Valuation.mem_valuationSubring_iff, Valuation.Integers.isIntegral_iff_v_le_one, ValuativeExtension.mapValueGroupWithZero_valuation, Valuation.isEquiv_iff_val_eq_one, WithVal.valueGroupEquiv_apply, Polynomial.valuation_inv_monomial_eq_valuation_X_zpow, Valuation.RankOne.strictMono, ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀, ValuationSubring.valuation_le_one_iff, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, ValuationSubring.mem_unitGroup_iff, Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk, Valued.isClosed_ball, Valuation.restrict_lt_one_iff, Valued.isClopen_sphere, inl_eq_coe_inlₗ, Valued.isClosed_sphere, IsValuativeTopology.isClosed_closedBall, Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, Valuation.cauchy_iff, IsValuativeTopology.mem_nhds_zero_iff, Valuation.IsRankOneDiscrete.generator_zpowers_eq_range, Valuation.IsRankOneDiscrete.embedding_generator', WithZeroTopology.isClosed_iff, WithZeroTopology.hasBasis_nhds_zero, ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, ValuationSubring.monotone_mapOfLE, Valuation.restrict_inj, Valuation.ltSubmodule_monotone, ValuativeRel.RankLeOneStruct.strictMono, Valued.integer.mulArchimedean_mrange_of_isCompact_integer, Valuation.embedding_restrict, Valuation.Integers.valuation_unit, Valued.closure_coe_completion_v_lt, Valued.valuation_isClosedMap, WithZeroTopology.nhds_coe_units, Valued.closure_coe_completion_v_mul_v_lt, Valued.cauchy_iff, Polynomial.valuation_le_one_of_valuation_X_le_one, ValuativeRel.one_apply_posSubmonoid, MonoidWithZeroHom.inr_mono, Valuation.extendToLocalization_mk', Valuation.IsRankOneDiscrete.generator'_zpowers_eq_top, Valuation.restrict_pos_iff, IsValuativeTopology.isClopen_ball, IsValuativeTopology.hasBasis_nhds, Valuation.restrict_def, Valued.toNormedField.one_lt_norm_iff, IsValuativeTopology.hasBasis_nhds_zero, Valuation.IsNontrivial_iff_exists_one_lt, Valuation.IsEquiv.orderMonoidIso_trans, WithVal.strictMono_valueGroupEquiv_symm, Valuation.mem_ltAddSubgroup_iff, Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup, Valuation.isClosed_closedBall, Valuation.map_inv, IsValuativeTopology.isOpen_closedBall, inr_eq_coe_inrₗ, Valuation.integer.v_irreducible_pos, Valuation.ltSubmodule_le_leSubmodule, Valuation.toTopologicalSpace_eq, ValuativeRel.exists_valuation_div_valuation_eq, Valuation.leIdeal_zero, Valuation.ltAddSubgroup_le_leAddSubgroup, fst_comp_inl, inv_mul_lt_of_lt_mul₀, Valuation.IsNontrivial.exists_one_lt, Polynomial.valuation_monomial_eq_valuation_X_pow, WithZeroTopology.isOpen_iff, WithZeroTopology.instContinuousMul, RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty, MonoidWithZeroHom.snd_mono, Valuation.IsUniformizer.val_pos, Valuation.isClopen_ball, Valuation.IsEquiv.val_sub_one_lt_one_iff, Valuation.Integers.valuation_pos_iff_ne_zero, Valued.isOpen_closedBall, Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial, Valuation.hasBasis_nhds, RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X, ValuativeRel.isNontrivial_iff_nontrivial_units, Valuation.ltSubmodule_v_le_of_mem, Valued.mem_nhds_zero, Valuation.RankLeOne.exists_val_lt, Valued.isOpen_ball, ValuationSubring.mem_principalUnitGroup_iff, Valued.mem_nhds, Polynomial.valuation_aeval_monomial_eq_valuation_pow, Valuation.isOpen_ball, Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer, wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero, ValuativeRel.ValueGroupWithZero.embed_mk, IsValuativeTopology.isClosed_ball, Valuation.Integer.not_isUnit_iff_valuation_lt_one, fst_apply, WithVal.valueGroupOrderIso₀_symm_restrict, Valuation.map_eq_one_of_forall_lt, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, Valuation.hasBasis_uniformity, Valued.toNormedField.norm_def, Valuation.toUniformSpace_eq, Valuation.isOpen_sphere, Valuation.norm_def, exists_pow_lt₀, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, Valuation.exists_div_eq_of_unit, Valuation.restrict_le_one_iff, Valuation.isClosed_ball, WithZeroTopology.tendsto_units, OrderIso.withZeroUnits_apply, Valuation.leAddSubgroup_zero, WithZeroTopology.Iio_mem_nhds_zero, Valuation.IsEquiv.orderMonoidIso_eq_refl, ValuationSubring.mem_nonunits_iff, Valuation.RankOne.zero_of_hom_zero, Valuation.IsEquiv.valueGroup₀Fun_zero, Valuation.IsEquiv.valueGroup₀Fun_spec, Valuation.Integers.valuation_irreducible_pos, MonoidWithZeroHom.inr_strictMono, Valuation.IsUniformizer.iff, Valued.hasBasis_uniformity, Valuation.mem_ltSubmodule_iff, ValuativeRel.valuation_lt_symm_orderMonoidIso, Valuation.integer.v_irreducible_lt_one, Valuation.IsNontrivial.exists_lt_one, Valuation.Integers.isUnit_iff_valuation_eq_one, Finset.sup_div₀, Valuation.restrict_lt_iff, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply, WithZeroTopology.tendsto_zero, Valued.isClosed_closedBall, Valuation.isOpen_closedBall, Valuation.coe_ltAddSubgroup, MonoidWithZeroHom.inl_mono, Valuation.RankOne.isNontrivial_restrict, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq, RatFunc.valuation_uniformizingPolynomial_lt_one, ValuativeRel.restrict_lt_orderMonoidIso, Valuation.one_le_val_iff, ValuationSubring.valuation_eq_one_iff, Valuation.norm_pos_iff_valuation_pos, Units.zero_lt, Valuation.ltIdeal_mono, Valuation.isEquiv_iff_val_lt_one, Valuation.IsUniformizer.val_lt_one, LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono, Valuation.restrict_exists_div_eq, Valuation.leSubmodule_zero, Valuation.mem_integer_iff, Units.mulArchimedean_iff, Valuation.IsEquiv.orderMonoidIso_spec, WithZeroTopology.singleton_mem_nhds_of_units, Valuation.RankOne.hom_eq_zero_iff, discrete_iff_not_denselyOrdered, Valued.isClopen_closedBall, Valuation.RankOne.restrict_RankOne_hom_eq, inl_apply, inr_apply, WithVal.strictMono_valueGroupEquiv, IsValuativeTopology.mem_nhds_iff, MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zero, Valuation.RankLeOne.strictMono', Valued.toNormedField.norm_lt_one_iff, denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units, Valuation.exists_setOf_restrict_le_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono, Valuation.Integers.one_of_isUnit, WithZeroTopology.nhds_eq_update, Real.exists_lt_of_strictMono, Valuation.IsRankOneDiscrete.exists_generator_lt_one, IsValuativeTopology.isOpen_sphere, ValuationSubring.mapOfLE_comp_valuation, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zpow, Valuation.val_le_one_iff, Valued.toNormedField.one_le_norm_iff, wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero, MonoidWithZeroHom.ValueGroup₀.embedding_strictMono, Valuation.IsRankOneDiscrete.generator_mem_range, IsValuativeTopology.isClopen_closedBall, Valuation.exists_div_eq_of_surjective, Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, Valuation.mem_nhds_iff, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange, Valuation.is_topological_valuation, Valuation.inversion_estimate, Valuation.isClopen_sphere, Valuation.IsEquiv.orderMonoidIso_symm, WithZero.withZeroUnitsEquiv_strictMono, discrete_or_denselyOrdered, Valuation.isClosed_sphere, WithZeroTopology.hasBasis_nhds_units, instDenselyOrderedUnits, WithZeroTopology.instContinuousInv₀, Valued.extensionValuation_toFun
toDiv 📖	CompOp	1 math math: div_eq_mul_inv
toInv 📖	CompOp	4 math math: mul_inv_cancel, inv_zero, div_eq_mul_inv, zpow_neg'
toLinearOrderedCommMonoidWithZero 📖	CompOp	414 math math: Valuation.mem_nhds_zero_iff, Valued.continuous_extension, Valuation.IsRankOneDiscrete.generator_lt_one, Valued.isOpen_closedball, Irreducible.maximalIdeal_eq_setOf_le_v_coe, Valuation.inversion_estimate', WithVal.valued_toVal, ValuationSubring.valuation_lt_one_iff, Valuation.leSubmodule_v_le_of_mem, WithVal.valueGroupOrderIso₀_symm_apply, Valuation.isEquiv_iff_val_sub_one_lt_one, Valuation.isClopen_closedBall, mul_inv_cancel, Valuation.mem_maximalIdeal_iff, Valuation.mem_leSubmodule_iff, Padic.withValUniformEquiv_norm_le_one_iff, Valued.toNormedField.norm_le_one_iff, Valued.extension_extends, WithVal.valueGroup_eq, Valued.valuedCompletion_surjective_iff, ValuativeRel.valuation_eq_zero_iff, ValuationSubring.valuation_le_iff, PadicComplex.valuation_extends, Valuation.IsRankOneDiscrete.exists_generator_lt_one', RatFunc.exists_zpow_uniformizingPolynomial, Valuation.Integers.one_of_isUnit', WithZeroTopology.nhds_zero, Valuation.isEquiv_valuation_valuationSubring, Valuation.mem_ltIdeal_iff, Valuation.val_le_one_or_val_inv_lt_one, WithVal.valueGroupOrderIso₀_restrict, Valuation.leSubmodule_monotone, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, WithVal.apply_ofVal, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, Valuation.IsRankOneDiscrete.generator_mem_valueGroup, MonoidWithZeroHom.ValueGroup₀.monoidWithZeroHom_strictMono, WithVal.valueGroupOrderIso₀_apply, Valuation.Integers.isPrincipal_iff_exists_isGreatest, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, inl_mul_inr_eq_coe_toLex, 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, ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl, Valuation.instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial, ValuationSubring.valuation_unit, NumberField.HeightOneSpectrum.rankOne_hom'_def, WithVal.valueGroupEquiv_symm_apply, Valuation.IsEquiv.valuedCompletion_le_one_iff, Valuation.restrict_eq_one_iff, Valuation.IsRankOneDiscrete.generator'_lt_one, Valuation.isNontrivial_iff_exists_lt_one, Valuation.Integers.valuation_irreducible_lt_one, WithZeroTopology.nhds_zero_of_units, ValuationSubring.mapOfLE_valuation_apply, RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one, WithVal.instCompatibleValuation, Valuation.Integers.map_le_one, zpow_zero', MonoidWithZeroHom.fst_mono, Valuation.IsEquiv.restrict, ValuativeRel.supp_eq_valuation_supp, Valuation.ltAddSubgroup_monotone, Valuation.ltIdeal_v_le_of_mem, Valued.isClopen_ball, ValuativeRel.ValueGroupWithZero.embed_strictMono, Valued.exists_coe_eq_v, ValuativeRel.ValueGroupWithZero.mk_eq_div, Valuation.Integers.le_of_dvd, Valuation.Compatible.ofValuation, Valuation.hasBasis_nhds_zero, WithZeroTopology.Iio_mem_nhds, Valuation.leIdeal_map_algebraMap_eq_leSubmodule_min, Valuation.val_lt_one_iff, Valuation.IsUniformizer.zpowers_eq_valueGroup, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀, Valuation.val_le_one_or_val_inv_le_one, Valuation.restrict_le_iff, ValuationSubring.eq_top_iff, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, Valuation.map_div, Valuation.restrict_eq_zero_iff, Valuation.one_lt_val_iff, Valuation.restrict_eq_mk, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, ValuationSubring.valuation_lt_one_or_eq_one, Valued.continuous_valuation, WithVal.apply_symm_equiv, Valuation.val_eq_one_iff, Valuation.restrict_lt_iff_lt_embedding, LaurentSeries.val_le_one_iff_eq_coe, Valued.extension_eq_zero_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos, WithVal.val_apply_equiv, IsValuativeTopology.isClopen_sphere, OrderMonoidIso.withZeroUnits_symm_apply, FunctionField.valuedFqtInfty.def, MonoidWithZeroHom.inl_strictMono, Valuation.HasExtension.ofComapInteger, WithZeroMulInt.toNNReal_lt_one_iff, Valuation.subgroups_basis, WithVal.apply_equiv, OrderMonoidIso.withZeroUnits_apply, Valuation.mem_unitGroup_iff, Valued.isOpen_sphere, Valuation.restrict_le_iff_le_embedding, IsDedekindDomain.HeightOneSpectrum.valuation_def, ValuationSubring.valuation_le_one, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, denselyOrdered_units_iff, OrderIso.withZeroUnits_symm_apply, Valuation.isEquiv_restrict, Valuation.nonempty_rankOne_iff_mulArchimedean, LaurentSeries.exists_ratFunc_val_lt, Valuation.RankOne.exists_val_lt, Valued.hasBasis_nhds_zero, Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup, IsValuativeTopology.continuous_valuation, IsValuativeTopology.mem_nhds_iff', mul_inv_lt_of_lt_mul₀, RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one, WithZero.withZeroUnitsEquiv_symm_strictMono, WithVal.strictMono_valueGroupOrderIso₀, Valuation.isEquiv_iff_val_le_one, WithVal.strictMono_valueGroupOrderIso₀_symm, Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing, Valuation.IsUniformizer.val, ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq, Valuation.mem_valuationSubring_iff, RatFunc.valuation_surjective, Valuation.Integers.isIntegral_iff_v_le_one, ValuativeExtension.mapValueGroupWithZero_valuation, Valuation.isEquiv_iff_val_eq_one, WithVal.valueGroupEquiv_apply, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered, Polynomial.valuation_inv_monomial_eq_valuation_X_zpow, Valuation.RankOne.strictMono, Valuation.Integers.le_iff_dvd, 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, Valued.isClosed_ball, Valuation.restrict_lt_one_iff, Valued.isClopen_sphere, PadicAlgCl.valuation_p, PadicComplex.valuation_p, inl_eq_coe_inlₗ, Valued.isClosed_sphere, IsValuativeTopology.isClosed_closedBall, WithZeroMulInt.toNNReal_le_one_iff, Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, WithVal.lt_def, Valuation.cauchy_iff, Valuation.locally_const, IsValuativeTopology.mem_nhds_zero_iff, ModP.preVal_mk, ModP.v_p_lt_preVal, Valuation.IsRankOneDiscrete.generator_zpowers_eq_range, Valuation.IsRankOneDiscrete.embedding_generator', WithZeroTopology.isClosed_iff, Valued.locally_const, WithZeroTopology.hasBasis_nhds_zero, Valuation.mem_leAddSubgroup_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, ValuationSubring.monotone_mapOfLE, Valued.toNormedField.norm_le_iff, Valuation.restrict_inj, Valuation.ltSubmodule_monotone, Valued.integer.mulArchimedean_mrange_of_isCompact_integer, Valuation.Integers.dvdNotUnit_iff_lt, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, Valuation.embedding_restrict, Valuation.Integers.valuation_unit, Valued.closure_coe_completion_v_lt, Valued.valuation_isClosedMap, Valuation.isEquiv_of_val_le_one, Valued.closure_coe_completion_v_mul_v_lt, Valued.valuedCompletion_apply, Valued.cauchy_iff, Polynomial.valuation_le_one_of_valuation_X_le_one, ValuationSubring.valuation_eq_iff, ValuativeRel.one_apply_posSubmonoid, Valuation.IsTrivialOn.of_le_one, ValuativeRel.trivialRel_eq_ofValuation_one, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, Valuation.leIdeal_v_le_of_mem, MonoidWithZeroHom.inr_mono, IsValuativeTopology.hasBasis_nhds_zero', Valuation.extendToLocalization_mk', Valuation.IsRankOneDiscrete.generator'_zpowers_eq_top, Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap, Valuation.RankOne.instIsNontrivial, Valuation.restrict_pos_iff, IsValuativeTopology.isClopen_ball, IsValuativeTopology.hasBasis_nhds, RatFunc.valuation_isEquiv_infty_or_adic, Valuation.restrict_def, Valued.toNormedField.one_lt_norm_iff, IsValuativeTopology.hasBasis_nhds_zero, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, Valuation.IsNontrivial_iff_exists_one_lt, Valuation.IsEquiv.orderMonoidIso_trans, WithVal.strictMono_valueGroupEquiv_symm, Valuation.mem_ltAddSubgroup_iff, Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup, LaurentSeries.valuation_LaurentSeries_equal_extension, Valuation.isClosed_closedBall, RatFunc.v_def, Valuation.map_inv, Valuation.Integers.wfDvdMonoid_iff_wellFounded_gt_on_v, Valuation.isNontrivial_valuation_valuationSubring_iff, IsValuativeTopology.isOpen_closedBall, inr_eq_coe_inrₗ, Valuation.integer.v_irreducible_pos, Valuation.leIdeal_mono, Valuation.toTopologicalSpace_eq, ValuativeRel.exists_valuation_div_valuation_eq, fst_comp_inl, inv_mul_lt_of_lt_mul₀, ValuativeRel.instCompatibleValueGroupWithZeroValuation, Valuation.IsNontrivial.exists_one_lt, PadicAlgCl.valuation_def, Polynomial.valuation_monomial_eq_valuation_X_pow, WithZeroTopology.isOpen_iff, Delone.DeloneSet.mapBilipschitz_trans, RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty, MonoidWithZeroHom.snd_mono, PadicAlgCl.valuation_coe, Valuation.IsUniformizer.val_pos, Valuation.isClopen_ball, FunctionField.inftyValuedFqt.def, Valuation.IsEquiv.val_sub_one_lt_one_iff, Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap, IsValuativeTopology.hasBasis_nhds', Valuation.Integers.valuation_pos_iff_ne_zero, Valued.isOpen_closedBall, Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial, Valuation.hasBasis_nhds, RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X, RatFunc.valuation_isEquiv_adic_of_not_isEquiv_infty, Valuation.ltSubmodule_v_le_of_mem, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, Valued.mem_nhds_zero, Valuation.RankLeOne.exists_val_lt, Valued.isOpen_ball, ValuationSubring.mem_principalUnitGroup_iff, NormedField.v_eq_valuation, Valued.mem_nhds, Polynomial.valuation_aeval_monomial_eq_valuation_pow, Valuation.isOpen_ball, IsNonarchimedeanLocalField.isCompact_closedBall, Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer, Valued.extensionValuation_apply_coe, ValuativeRel.valuation_surjective, wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero, LaurentSeries.valuation_surjective, LaurentSeries.valuation_coe_ratFunc, ValuativeRel.ValueGroupWithZero.embed_mk, Valuation.Integers.isPrincipal_iff_exists_eq_setOf_valuation_le, IsValuativeTopology.isClosed_ball, Valuation.Integer.not_isUnit_iff_valuation_lt_one, fst_apply, PadicComplex.RankOne.hom_eq_embedding, WithVal.valueGroupOrderIso₀_symm_restrict, Valuation.map_eq_one_of_forall_lt, LaurentSeries.valuation_compare, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply, Valuation.RankOne.toIsNontrivial, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, Valuation.hasBasis_uniformity, WithZeroMulInt.toNNReal_strictMono, Valued.toNormedField.norm_def, LaurentSeries.tendsto_valuation, Valuation.toUniformSpace_eq, Valuation.isOpen_sphere, Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe, Valuation.norm_def, exists_pow_lt₀, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, lt_of_mul_lt_mul_of_le₀, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', Valuation.exists_div_eq_of_unit, Valuation.restrict_le_one_iff, Valuation.isClosed_ball, OrderIso.withZeroUnits_apply, WithZeroTopology.Iio_mem_nhds_zero, RatFunc.valuation_isEquiv_inftyValuation_of_one_lt_valuation_X, Valuation.IsEquiv.orderMonoidIso_eq_refl, Valuation.HasExtension.mk_smul_mk, inv_zero, zpow_succ', ValuationSubring.mem_nonunits_iff, Valued.toNormedField.norm_lt_iff, Valuation.RankOne.zero_of_hom_zero, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, Valuation.IsEquiv.valueGroup₀Fun_zero, Valuation.IsEquiv.valueGroup₀Fun_spec, Valuation.Integers.valuation_irreducible_pos, MonoidWithZeroHom.inr_strictMono, Valuation.IsUniformizer.iff, Valued.hasBasis_uniformity, Valuation.mem_ltSubmodule_iff, ModP.v_p_lt_val, ValuativeRel.valuation_lt_symm_orderMonoidIso, Valuation.integer.v_irreducible_lt_one, Valuation.IsNontrivial.exists_lt_one, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, Valuation.Integers.isUnit_iff_valuation_eq_one, Finset.sup_div₀, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, Valuation.restrict_lt_iff, Valuation.extendToLocalization_apply_map_apply, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply, IsNonarchimedeanLocalField.instCompatibleValueGroupWithZeroV, Valuation.mem_leIdeal_iff, WithZeroTopology.tendsto_zero, Valued.isClosed_closedBall, Valuation.isOpen_closedBall, PreTilt.map_eq_zero, Valuation.coe_ltAddSubgroup, MonoidWithZeroHom.inl_mono, RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one, Valuation.RankOne.isNontrivial_restrict, WithZeroTopology.orderClosedTopology, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq, WithVal.le_def, RatFunc.valuation_uniformizingPolynomial_lt_one, ValuativeRel.restrict_lt_orderMonoidIso, Valuation.one_le_val_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, ValuationSubring.valuation_eq_one_iff, WithZeroTopology.isOpen_Iio, Valuation.norm_pos_iff_valuation_pos, Valuation.isEquiv_tfae, Valuation.valuationSubring_eq_top_iff, ValuativeRel.ValueGroupWithZero.lift_valuation, Units.zero_lt, Valuation.ltIdeal_mono, Valued.continuous_valuation_of_surjective, Valuation.isEquiv_iff_val_lt_one, WithVal.valuation_equiv_symm, NormedField.valuation_apply, Valuation.IsUniformizer.val_lt_one, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono, div_eq_mul_inv, Valuation.restrict_exists_div_eq, Valuation.mem_integer_iff, Units.mulArchimedean_iff, Valuation.IsEquiv.orderMonoidIso_spec, Valuation.RankOne.hom_eq_zero_iff, discrete_iff_not_denselyOrdered, Valued.isClopen_closedBall, Valuation.RankOne.restrict_RankOne_hom_eq, inl_apply, Valuation.leAddSubgroup_monotone, inr_apply, WithVal.strictMono_valueGroupEquiv, IsValuativeTopology.mem_nhds_iff, ValuationSubring.valuation_surjective, MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid, Valuation.IsRankOneDiscrete.instIsNontrivial, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zero, Valued.exists_pow_lt_of_le_exp_neg_one, Valuation.RankLeOne.strictMono', Valued.toNormedField.norm_lt_one_iff, denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units, Valuation.exists_setOf_restrict_le_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono, Valuation.Integers.one_of_isUnit, WithZeroTopology.nhds_eq_update, Valuation.IsRankOneDiscrete.exists_generator_lt_one, IsValuativeTopology.isOpen_sphere, ValuationSubring.mapOfLE_comp_valuation, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zpow, Valuation.val_le_one_iff, LaurentSeries.exists_ratFunc_eq_v, Valued.toNormedField.one_le_norm_iff, wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero, MonoidWithZeroHom.ValueGroup₀.embedding_strictMono, ValuativeRel.ValueGroupWithZero.mk_eq_valuation, Valuation.coeff_zero_minpoly, Valuation.IsRankOneDiscrete.generator_mem_range, IsValuativeTopology.isClopen_closedBall, Valuation.exists_div_eq_of_surjective, Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, Valuation.mem_nhds_iff, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange, LaurentSeries.valuation_X_pow, Valuation.Integers.dvd_iff_le, NumberField.FinitePlace.norm_def, Valuation.is_topological_valuation, Valuation.inversion_estimate, Valuation.isClopen_sphere, Valuation.isNontrivial_iff_not_a_field, Valuation.IsEquiv.orderMonoidIso_symm, WithZero.withZeroUnitsEquiv_strictMono, discrete_or_denselyOrdered, Valuation.isClosed_sphere, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, instDenselyOrderedUnits, Valued.extensionValuation_toFun, Valuation.isEquiv_iff_valuationSubring
zpow 📖	CompOp	3 math math: zpow_zero', zpow_succ', zpow_neg'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_eq_mul_inv 📖	mathematical	—	toDiv Semigroup.toMul Monoid.toSemigroup CommMonoid.toMonoid CommMonoidWithZero.toCommMonoid LinearOrderedCommMonoidWithZero.toCommMonoidWithZero toLinearOrderedCommMonoidWithZero toInv	—	—
inv_zero 📖	mathematical	—	toInv CommMonoidWithZero.toZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero toLinearOrderedCommMonoidWithZero	—	—
mul_inv_cancel 📖	mathematical	—	Semigroup.toMul Monoid.toSemigroup CommMonoid.toMonoid CommMonoidWithZero.toCommMonoid LinearOrderedCommMonoidWithZero.toCommMonoidWithZero toLinearOrderedCommMonoidWithZero toInv Monoid.toOne	—	—
toNontrivial 📖	mathematical	—	Nontrivial	—	—
zpow_neg' 📖	mathematical	—	zpow toInv	—	—
zpow_succ' 📖	mathematical	—	zpow Semigroup.toMul Monoid.toSemigroup CommMonoid.toMonoid CommMonoidWithZero.toCommMonoid LinearOrderedCommMonoidWithZero.toCommMonoidWithZero toLinearOrderedCommMonoidWithZero	—	—
zpow_zero' 📖	mathematical	—	zpow Monoid.toOne CommMonoid.toMonoid CommMonoidWithZero.toCommMonoid LinearOrderedCommMonoidWithZero.toCommMonoidWithZero toLinearOrderedCommMonoidWithZero	—	—

LinearOrderedCommMonoidWithZero

Definitions

Name	Category	Theorems
toCommMonoidWithZero 📖	CompOp	89 math math: Valuation.IsTrivialOn.valuation_algebraMap_le_one, ofDual_toAdd_zero, Valuation.FiniteField.algebraMap_le_one, Valuation.FiniteField.algebraMap_eq_one, Valuation.one_apply_lt_one_iff, LinearOrderedCommGroupWithZero.mul_inv_cancel, Valuation.val_mrange_zero, Valuation.map_one_add_of_lt, Valuation.mem_supp_iff, Valuation.isEquiv_map_self_of_strictMono, Valuation.IsTrivialOn.eq_one, Valuation.toFun_eq_coe, le_zero_iff, ValuationClass.toMonoidWithZeroHomClass, LinearOrderedCommGroupWithZero.zpow_zero', Valuation.IsEquiv.pos_iff, Valuation.unit_map_eq, Valuation.one_apply_of_ne_zero, OrderMonoidWithZeroHom.mul_comp, Valuation.coe_coe, ofAdd_bot, Valuation.IsEquiv.one_lt_iff_one_lt, Valuation.nonempty_rankOne_iff_mulArchimedean, toIsOrderedMonoid, Valuation.toMonoidWithZeroHom_one, Valuation.HasExtension.val_map_le_one_iff, Valuation.map_add_le_max', Valuation.zero_iff, FiniteField.valuation_algebraMap_eq_one, Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, Valuation.one_apply_eq_zero_iff, Valuation.apply_posSubmonoid_pos, Valuation.one_srel_iff, Valued.integer.mulArchimedean_mrange_of_isCompact_integer, Padic.valuation_p_lt_one, Valuation.map_mul, Valuation.one_apply_le_one, Valuation.map_one_sub_of_lt, Valuation.map_one, Valuation.one_vlt_iff, Valuation.one_vle_iff, Valuation.IsEquiv.eq_zero, Valuation.map_apply, not_lt_zero', Valuation.toMonoidWithZeroHom_coe_eq_coe, Valuation.srel_one_iff, Valuation.vle_one_iff, Valuation.IsEquiv.one_le_iff_one_le, Valuation.HasExtension.val_map_eq_one_iff, OrderMonoidWithZeroHom.coe_mul, zero_le, ofDual_toAdd_eq_top_iff, Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer, Valuation.rel_one_iff, Valuation.IsEquiv.eq_one_iff_eq_one, Valuation.vlt_one_iff, Valuation.IsEquiv.le_one_iff_le_one, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, zero_le', toIsMulTorsionFree, Valuation.HasExtension.mk_smul_mk, LinearOrderedCommGroupWithZero.inv_zero, LinearOrderedCommGroupWithZero.zpow_succ', Valuation.map_pow, Valuation.IsEquiv.valueGroup₀Fun_spec, zero_lt_iff, toMulPosStrictMono, FiniteField.valuation_algebraMap_le_one, pow_pos_iff, instIsCancelMulZero_1, bot_eq_zero'', Valuation.HasExtension.val_map_lt_one_iff, Valuation.coe_mk, OrderMonoidWithZeroHom.comp_mul, Valuation.IsEquiv.lt_one_iff_lt_one, LinearOrderedCommGroupWithZero.div_eq_mul_inv, Valuation.one_apply_def, Units.mulArchimedean_iff, Valuation.pos_iff, MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid, Valuation.map_zero, ofAdd_toDual_eq_zero_iff, toPosMulStrictMono, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange, OrderMonoidWithZeroHom.mul_apply, Valuation.one_rel_iff, Valuation.le_one_of_subsingleton, Valuation.one_apply_eq_one_iff, toZeroLeOneClass
toLinearOrder 📖	CompOp	273 math math: Valuation.mem_nhds_zero_iff, Valuation.IsRankOneDiscrete.generator_lt_one, Valued.isOpen_closedball, Valuation.IsTrivialOn.valuation_algebraMap_le_one, Irreducible.maximalIdeal_eq_setOf_le_v_coe, Valuation.inversion_estimate', ValuationSubring.valuation_lt_one_iff, Valuation.FiniteField.algebraMap_le_one, WithVal.valueGroupOrderIso₀_symm_apply, Valuation.HasExtension.val_map_le_iff, Valuation.isEquiv_iff_val_sub_one_lt_one, Valuation.one_apply_lt_one_iff, Valuation.isClopen_closedBall, Valuation.mem_maximalIdeal_iff, Valuation.mem_leSubmodule_iff, Valuation.isEquiv_map_self_of_strictMono, Valued.toNormedField.norm_le_one_iff, ValuationSubring.valuation_le_iff, Valuation.IsRankOneDiscrete.exists_generator_lt_one', WithZeroTopology.nhds_zero, Valuation.mem_ltIdeal_iff, Valuation.val_le_one_or_val_inv_lt_one, WithVal.valueGroupOrderIso₀_restrict, Valuation.leSubmodule_monotone, MonoidWithZeroHom.ValueGroup₀.monoidWithZeroHom_strictMono, WithVal.valueGroupOrderIso₀_apply, Valuation.Integers.isPrincipal_iff_exists_isGreatest, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero, le_zero_iff, Valuation.Compatible.srel_iff_lt, Valuation.IsEquiv.valuedCompletion_le_one_iff, Valuation.isEquiv_iff_val_lt_val, Valuation.IsRankOneDiscrete.generator'_lt_one, Valuation.isNontrivial_iff_exists_lt_one, Valuation.Integers.valuation_irreducible_lt_one, WithZeroTopology.nhds_zero_of_units, Valuation.Integers.map_le_one, MonoidWithZeroHom.fst_mono, Valuation.ltAddSubgroup_monotone, Valued.isClopen_ball, ValuativeRel.ValueGroupWithZero.embed_strictMono, Valuation.IsEquiv.pos_iff, Valuation.Integers.le_of_dvd, Valuation.hasBasis_nhds_zero, WithZeroTopology.Iio_mem_nhds, Valuation.leIdeal_map_algebraMap_eq_leSubmodule_min, Valuation.val_lt_one_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀, Valuation.val_le_one_or_val_inv_le_one, Valuation.map_add_of_distinct_val, Valuation.restrict_le_iff, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono, Valuation.map_add, Valuation.HasExtension.val_map_lt_iff, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, Valuation.one_lt_val_iff, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, ValuationSubring.valuation_lt_one_or_eq_one, OrderMonoidWithZeroHom.mul_comp, Valuation.restrict_lt_iff_lt_embedding, MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos, OrderMonoidIso.withZeroUnits_symm_apply, MonoidWithZeroHom.inl_strictMono, OrderMonoidIso.withZeroUnits_apply, Valuation.IsEquiv.one_lt_iff_one_lt, Valuation.map_add_le, Valuation.restrict_le_iff_le_embedding, ValuationClass.map_add_le_max, ValuationSubring.valuation_le_one, denselyOrdered_units_iff, OrderIso.withZeroUnits_symm_apply, Valuation.nonempty_rankOne_iff_mulArchimedean, toIsOrderedMonoid, Valued.hasBasis_nhds_zero, mul_inv_lt_of_lt_mul₀, WithZero.withZeroUnitsEquiv_symm_strictMono, WithVal.strictMono_valueGroupOrderIso₀, Valuation.isEquiv_iff_val_le_one, WithVal.strictMono_valueGroupOrderIso₀_symm, Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing, Valuation.HasExtension.val_map_le_one_iff, Valuation.map_sub, Valuation.mem_valuationSubring_iff, Valuation.Integers.isIntegral_iff_v_le_one, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered, Valuation.RankOne.strictMono, Valuation.Integers.le_iff_dvd, ValuationSubring.valuation_le_one_iff, Valuation.map_add_le_max', ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk, Valued.isClosed_ball, Valuation.restrict_lt_one_iff, Valuation.map_sub_le, Valuation.srel_iff_lt, LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ, IsValuativeTopology.isClosed_closedBall, Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, WithVal.lt_def, Valuation.cauchy_iff, Valuation.apply_posSubmonoid_pos, Valuation.one_srel_iff, WithZeroTopology.isClosed_iff, WithZeroTopology.hasBasis_nhds_zero, Valuation.mem_leAddSubgroup_iff, Valuation.vle_iff_le, ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, ValuationSubring.monotone_mapOfLE, Valued.toNormedField.norm_le_iff, Valuation.map_add', Valuation.ltSubmodule_monotone, Valuation.map_sum_lt, Valuation.map_add_lt, Valued.integer.mulArchimedean_mrange_of_isCompact_integer, Valuation.Integers.dvdNotUnit_iff_lt, Padic.valuation_p_lt_one, Valuation.IsEquiv.lt_iff_lt, Valuation.map_sum_lt', Valued.closure_coe_completion_v_lt, Valued.closure_coe_completion_v_mul_v_lt, Valued.cauchy_iff, Valuation.one_apply_le_one, Polynomial.valuation_le_one_of_valuation_X_le_one, MonoidWithZeroHom.inr_mono, Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap, Valuation.restrict_pos_iff, Valuation.one_vlt_iff, IsValuativeTopology.isClopen_ball, Valuation.one_vle_iff, Valued.toNormedField.one_lt_norm_iff, Valuation.IsNontrivial_iff_exists_one_lt, Valuation.IsEquiv.orderMonoidIso_trans, WithVal.strictMono_valueGroupEquiv_symm, Valuation.mem_ltAddSubgroup_iff, Valuation.isClosed_closedBall, Valuation.Integers.wfDvdMonoid_iff_wellFounded_gt_on_v, IsValuativeTopology.isOpen_closedBall, LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ, Valuation.integer.v_irreducible_pos, Valuation.leIdeal_mono, LinearOrderedCommGroupWithZero.fst_comp_inl, inv_mul_lt_of_lt_mul₀, Valuation.IsNontrivial.exists_one_lt, not_lt_zero', WithZeroTopology.isOpen_iff, Valuation.srel_one_iff, RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty, MonoidWithZeroHom.snd_mono, Valuation.IsUniformizer.val_pos, Valuation.isClopen_ball, Valuation.vle_one_iff, Valuation.IsEquiv.val_sub_one_lt_one_iff, Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap, Valuation.Integers.valuation_pos_iff_ne_zero, Valued.isOpen_closedBall, Valuation.hasBasis_nhds, Valuation.IsEquiv.one_le_iff_one_le, Valued.mem_nhds_zero, Valued.isOpen_ball, ValuationSubring.mem_principalUnitGroup_iff, Valued.mem_nhds, OrderMonoidWithZeroHom.coe_mul, zero_le, Valuation.IsEquiv.le_iff_le, Valuation.isOpen_ball, Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer, Valuation.rel_one_iff, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero, Valuation.Integers.isPrincipal_iff_exists_eq_setOf_valuation_le, IsValuativeTopology.isClosed_ball, Valuation.Integer.not_isUnit_iff_valuation_lt_one, LinearOrderedCommGroupWithZero.fst_apply, WithVal.valueGroupOrderIso₀_symm_restrict, Valuation.vlt_one_iff, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, Valuation.hasBasis_uniformity, Valuation.IsEquiv.le_one_iff_le_one, Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe, exists_pow_lt₀, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, lt_of_mul_lt_mul_of_le₀, zero_le', Valuation.exists_div_eq_of_unit, Valuation.restrict_le_one_iff, Valuation.isClosed_ball, OrderIso.withZeroUnits_apply, WithZeroTopology.Iio_mem_nhds_zero, Valuation.IsEquiv.orderMonoidIso_eq_refl, Valuation.HasExtension.mk_smul_mk, ValuationSubring.mem_nonunits_iff, Valued.toNormedField.norm_lt_iff, Valuation.rel_iff_le, Valuation.Integers.valuation_irreducible_pos, Valuation.vlt_iff_lt, MonoidWithZeroHom.inr_strictMono, Valued.hasBasis_uniformity, Valuation.mem_ltSubmodule_iff, ValuativeRel.valuation_lt_symm_orderMonoidIso, zero_lt_iff, Valuation.integer.v_irreducible_lt_one, toMulPosStrictMono, Valuation.IsNontrivial.exists_lt_one, FiniteField.valuation_algebraMap_le_one, pow_pos_iff, Finset.sup_div₀, Valuation.restrict_lt_iff, Valuation.mem_leIdeal_iff, WithZeroTopology.tendsto_zero, Valued.isClosed_closedBall, Valuation.isOpen_closedBall, Valuation.coe_ltAddSubgroup, MonoidWithZeroHom.inl_mono, WithZeroTopology.orderClosedTopology, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, bot_eq_zero'', WithVal.le_def, RatFunc.valuation_uniformizingPolynomial_lt_one, Valuation.HasExtension.val_map_lt_one_iff, ValuativeRel.restrict_lt_orderMonoidIso, Valuation.one_le_val_iff, Valuation.Compatible.vle_iff_le, WithZeroTopology.isOpen_Iio, Valuation.norm_pos_iff_valuation_pos, Valuation.map_sub_lt, Valuation.map_sum_le, Units.zero_lt, OrderMonoidWithZeroHom.comp_mul, Valuation.ltIdeal_mono, Valuation.IsEquiv.lt_one_iff_lt_one, Valuation.isEquiv_iff_val_lt_one, Valuation.IsUniformizer.val_lt_one, LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono, Valuation.restrict_exists_div_eq, Valuation.mem_integer_iff, Units.mulArchimedean_iff, Valuation.IsEquiv.orderMonoidIso_spec, LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered, Valued.isClopen_closedBall, LinearOrderedCommGroupWithZero.inl_apply, Valuation.leAddSubgroup_monotone, LinearOrderedCommGroupWithZero.inr_apply, WithVal.strictMono_valueGroupEquiv, Valuation.pos_iff, MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid, Valuation.RankLeOne.strictMono', Valued.toNormedField.norm_lt_one_iff, denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units, Valuation.exists_setOf_restrict_le_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono, WithZeroTopology.nhds_eq_update, Valuation.IsRankOneDiscrete.exists_generator_lt_one, Valuation.val_le_one_iff, Valued.toNormedField.one_le_norm_iff, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero, MonoidWithZeroHom.ValueGroup₀.embedding_strictMono, IsValuativeTopology.isClopen_closedBall, Valuation.exists_div_eq_of_surjective, Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, toPosMulStrictMono, Valuation.mem_nhds_iff, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange, Valuation.Integers.dvd_iff_le, OrderMonoidWithZeroHom.mul_apply, Valuation.is_topological_valuation, Valuation.one_rel_iff, Valuation.le_one_of_subsingleton, Valuation.inversion_estimate, Valuation.IsEquiv.orderMonoidIso_symm, WithZero.withZeroUnitsEquiv_strictMono, LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered, instDenselyOrderedUnits, toZeroLeOneClass
toOrderBot 📖	CompOp	2 math math: Finset.sup_div₀, bot_eq_zero''

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsMulTorsionFree 📖	mathematical	—	IsMulTorsionFree MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero toCommMonoidWithZero	—	StrictMonoOn.injOn pow_left_strictMonoOn₀ toPosMulStrictMono MulPosStrictMono.toMulPosMono toMulPosStrictMono
toIsOrderedMonoid 📖	mathematical	—	IsOrderedMonoid CommMonoidWithZero.toCommMonoid toCommMonoidWithZero PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder toLinearOrder	—	eq_or_ne MulZeroClass.mul_zero instReflLe LE.le.eq_or_lt LT.lt.le mul_lt_mul_of_pos_right toMulPosStrictMono zero_lt_iff
toMulPosStrictMono 📖	mathematical	—	MulPosStrictMono MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero toCommMonoidWithZero MulZeroClass.toZero PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder toLinearOrder	—	posMulStrictMono_iff_mulPosStrictMono CommMagma.to_isCommutative toPosMulStrictMono
toPosMulStrictMono 📖	mathematical	—	PosMulStrictMono Semigroup.toMul Monoid.toSemigroup CommMonoid.toMonoid CommMonoidWithZero.toCommMonoid toCommMonoidWithZero CommMonoidWithZero.toZero PartialOrder.toPreorder LinearOrder.toPartialOrder toLinearOrder	—	—
toZeroLeOneClass 📖	mathematical	—	ZeroLEOneClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero toCommMonoidWithZero MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder toLinearOrder	—	zero_le'
zero_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder toLinearOrder CommMonoidWithZero.toZero toCommMonoidWithZero	—	—

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zero_lt 📖	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 val MonoidWithZero.toMonoid	—	zero_lt_iff ne_zero GroupWithZero.toNontrivial

WithZero

Definitions

Name	Category	Theorems
decidableEq 📖	CompOp	—
decidableLE 📖	CompOp	—
decidableLT 📖	CompOp	—
expOrderIso 📖	CompOp	3 math math: val_expOrderIso_apply, expOrderIso_symm_apply, val_inv_expOrderIso_apply
instBot 📖	CompOp	1 math math: zero_eq_bot
instBoundedOrder 📖	CompOp	—
instLT 📖	CompOp	12 math math: lt_iff_exists, lt_iff_exists_coe, pos_iff_ne_zero, one_lt_coe, not_lt_zero, coe_lt_one, lt_unzero_iff, zero_lt_coe, unzero_lt_iff, coe_lt_coe, lt_coe_iff, lt_def
instLattice 📖	CompOp	—
instLinearOrder 📖	CompOp	—
instLinearOrderedCommGroupWithZero 📖	CompOp	115 math math: IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', ValuationSubring.integralClosure_algebraMap_injective, NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, Set.unit_eq, NumberField.FinitePlace.norm_def', IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, NumberField.FinitePlace.embedding_apply, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, LaurentSeries.valuation_single_zpow, NumberField.HeightOneSpectrum.rankOne_hom'_def, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', NumberField.FinitePlace.norm_embedding_eq, LaurentSeries.inducing_coe, LaurentSeries.continuous_coe, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, NumberField.FinitePlace.norm_embedding, LaurentSeries.val_le_one_iff_eq_coe, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDiscreteValuationRing.isRankOneDiscrete, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, Valued.tendsto_zero_pow_of_le_exp_neg_one, FunctionField.valuedFqtInfty.def, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, IsDedekindDomain.HeightOneSpectrum.valuation_def, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_1, LaurentSeries.exists_ratFunc_val_lt, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, NumberField.FinitePlace.norm_lt_one_iff_mem, RatFunc.valuation_surjective, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', ValuationSubring.instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, PadicInt.coe_adicCompletionIntegersEquiv_apply, LaurentSeries.coe_X_compare, NumberField.HeightOneSpectrum.embedding_mul_absNorm, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.continuous_coe', NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, NumberField.FinitePlace.norm_def_int, ValuationSubring.isIntegral_of_mem_ringOfIntegers', IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, LaurentSeries.valuation_LaurentSeries_equal_extension, RatFunc.v_def, LaurentSeries.LaurentSeries_coe, LaurentSeries.powerSeries_ext_subring, NumberField.HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers, ValuationSubring.isIntegral_of_mem_ringOfIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, FunctionField.inftyValuedFqt.def, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, LaurentSeries.instLaurentSeriesComplete, Padic.withValUniformEquiv_cast_apply, LaurentSeries.valuation_surjective, LaurentSeries.valuation_coe_ratFunc, Padic.coe_withValRingEquiv, NumberField.FinitePlace.norm_eq_one_iff_notMem, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, LaurentSeries.tendsto_valuation, LaurentSeries.coe_range_dense, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', Padic.coe_withValRingEquiv_symm, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, LaurentSeries.comparePkg_eq_extension, LaurentSeries.valuation_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, LaurentSeries.uniformContinuous_coeff, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, Set.integer_eq, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, NumberField.FinitePlace.norm_embedding', NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, Valuation.IsRankOneDiscrete.generator_eq_neg_exp_one_of_surjective, ValuationSubring.algebraMap_injective, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, Valued.exists_pow_lt_of_le_exp_neg_one, instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, NumberField.FinitePlace.norm_embedding_int, LaurentSeries.exists_ratFunc_eq_v, Padic.isDenseInducing_cast_withVal, LaurentSeries.uniformContinuous_withVal_equiv, LaurentSeries.valuation_X_pow, NumberField.FinitePlace.norm_def, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers
instLinearOrderedCommMonoidWithZero 📖	CompOp	87 math math: Rat.padicValuation_cast, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff_mem_primeCompl, WeierstrassCurve.HasAdditiveReduction.badReduction, Padic.instCompatibleWithZeroMultiplicativeIntMulValuation, NumberField.FinitePlace.norm_def', FunctionField.inftyValuation.X_inv, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, Int.padicValuation_lt_one_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, IsDedekindDomain.HeightOneSpectrum.intValuation_le_one, WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral, IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntValuation, Int.padicValuation_eq_one_iff, RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem, IsDedekindDomain.HeightOneSpectrum.intValuation_singleton, FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation, Rat.padicValuation_self, Polynomial.valuation_of_mk, WeierstrassCurve.hasGoodReduction_iff, RatFunc.adicValuation_not_isEquiv_infty_valuation, WeierstrassCurve.hasMultiplicativeReduction_iff, Padic.norm_eq_zpow_log_mulValuation, PowerSeries.intValuation_eq_of_coe, FunctionField.instIsTrivialOnWithZeroMultiplicativeIntRatFuncInftyValuation, NumberField.HeightOneSpectrum.adicAbv_def, IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, IsDedekindDomain.HeightOneSpectrum.valuation_def, Padic.mulValuation_toFun, IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff, RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one, WeierstrassCurve.HasGoodReduction.goodReduction, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd, Padic.comap_mulValuation_eq_padicValuation, Rat.valuation_le_one_iff_den, LaurentSeries.exists_Polynomial_intValuation_lt, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', RatFunc.valuation_eq_LaurentSeries_valuation, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, Int.padicValuation_self, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, NumberField.FinitePlace.norm_def_int, WeierstrassCurve.hasAdditiveReduction_iff, WeierstrassCurve.HasAdditiveReduction.additiveReduction, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd, RatFunc.valuation_isEquiv_infty_or_adic, IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, RatFunc.v_def, Rat.padicValuation_eq_zero_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff, Set.unit_valuation_eq_one, FunctionField.inftyValuation.X_zpow, IsDedekindDomain.HeightOneSpectrum.intValuation_def, FunctionField.inftyValuation.X, RatFunc.valuation_isEquiv_adic_of_not_isEquiv_infty, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq, IsDedekindDomain.HeightOneSpectrum.valuation_surjective, Padic.comap_mulValuation_eq_int_padicValuation, PowerSeries.intValuation_X, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', RatFunc.valuation_isEquiv_inftyValuation_of_one_lt_valuation_X, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntIntValuation, FunctionField.inftyValuation.C, Rat.HeightOneSpectrum.valuation_equiv_padicValuation, Padic.norm_rat_le_one_iff_padicValuation_le_one, Set.integer_valuation_le_one, Rat.surjective_padicValuation, IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer, Int.padicValuation_le_one, NumberField.FinitePlace.norm_embedding', WeierstrassCurve.HasMultiplicativeReduction.badReduction, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq, FunctionField.inftyValuation_apply, NumberField.FinitePlace.norm_embedding_int, IsDedekindDomain.HeightOneSpectrum.intValuation_apply, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem, Int.padicValuation_eq_zero_iff, WeierstrassCurve.HasMultiplicativeReduction.multiplicativeReduction, Rat.padicValuation_le_one_iff, Polynomial.valuation_X_eq_neg_one
instOrderBot 📖	CompOp	—
instPartialOrder 📖	CompOp	3 math math: mulArchimedean_iff, Valuation.nonempty_rankOne_iff_mulArchimedean, instMulArchimedean
instPreorder 📖	CompOp	187 math math: Valuation.mem_nhds_zero_iff, logOrderIso_apply, Valued.isOpen_closedball, instExistsAddOfLE, OrderMonoidIso.val_inv_unitsWithZero_symm_apply, val_expOrderIso_apply, WithVal.valueGroupOrderIso₀_symm_apply, instPosMulMonoWithZeroOfMulLeftMono, Valuation.isClopen_closedBall, map'_mono, isOrderedMonoid, Padic.withValUniformEquiv_norm_le_one_iff, WeierstrassCurve.HasAdditiveReduction.badReduction, OrderMonoidIso.withZero_symm_apply_symm_apply, OrderMonoidIso.withZero_symm_apply_apply, WithVal.valueGroupOrderIso₀_restrict, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, Int.padicValuation_lt_one_iff, MonoidWithZeroHom.ValueGroup₀.monoidWithZeroHom_strictMono, WithVal.valueGroupOrderIso₀_apply, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, exp_lt_exp, log_le_log, IsDedekindDomain.HeightOneSpectrum.intValuation_le_one, WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral, map'_strictMono, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem, MonoidWithZeroHom.fst_mono, Valued.isClopen_ball, ValuativeRel.ValueGroupWithZero.embed_strictMono, isOrderedAddMonoid, Valuation.hasBasis_nhds_zero, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀, log_le_iff_le_exp, expOrderIso_symm_apply, Valuation.restrict_le_iff, ValuativeRel.nonempty_orderIso_withZeroMul_int_iff, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, lt_ofAdd_iff, WeierstrassCurve.hasMultiplicativeReduction_iff, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, Valuation.restrict_lt_iff_lt_embedding, LaurentSeries.val_le_one_iff_eq_coe, lt_mul_exp_iff_le, OrderMonoidIso.withZeroUnits_symm_apply, MonoidWithZeroHom.inl_strictMono, WithZeroMulInt.toNNReal_lt_one_iff, OrderMonoidIso.withZeroUnits_apply, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, Valuation.restrict_le_iff_le_embedding, OrderMonoidIso.val_unitsWithZero_symm_apply, OrderIso.withZeroUnits_symm_apply, FunctionField.InftyValuation.map_add_le_max', WeierstrassCurve.IsMinimal.val_Δ_maximal, LaurentSeries.exists_ratFunc_val_lt, Valued.hasBasis_nhds_zero, IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd, withZeroUnitsEquiv_symm_strictMono, WithVal.strictMono_valueGroupOrderIso₀, IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max', OrderMonoidIso.withZero_apply_symm_apply, WithVal.strictMono_valueGroupOrderIso₀_symm, Rat.valuation_le_one_iff_den, le_max_iff, Valuation.RankOne.strictMono, LaurentSeries.exists_Polynomial_intValuation_lt, exp_le_exp, toMulBot_lt, ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk, Valued.isClosed_ball, exists_ne_zero_and_le_and_le, instDenselyOrderedWithZeroOfNoMinOrder, Valuation.restrict_lt_one_iff, exists_ne_zero_and_lt_and_lt, LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ, OrderMonoidIso.unitsWithZero_apply, IsValuativeTopology.isClosed_closedBall, WithZeroMulInt.toNNReal_le_one_iff, val_inv_expOrderIso_apply, Valuation.cauchy_iff, exists_ne_zero_and_lt, log_lt_log, OrderMonoidIso.withZero_apply_apply, ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, le_exp_of_log_le, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, instMulLeftMono, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, le_ofAdd_of_toAdd_unzero_le, Valued.cauchy_iff, le_log_iff_exp_le, MonoidWithZeroHom.inr_mono, WeierstrassCurve.hasAdditiveReduction_iff, WeierstrassCurve.HasAdditiveReduction.additiveReduction, instMulLeftReflectLT, lt_exp_of_log_lt, Valuation.restrict_pos_iff, IsValuativeTopology.isClopen_ball, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd, denselyOrdered_set_iff_subsingleton, IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt, Valuation.IsEquiv.orderMonoidIso_trans, Valuation.isClosed_closedBall, WeierstrassCurve.isMinimal_iff, instMulPosMonoWithZeroOfMulRightMono, IsValuativeTopology.isOpen_closedBall, le_ofAdd_iff, LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ, lt_log_iff_exp_lt, LinearOrderedCommGroupWithZero.fst_comp_inl, MonoidWithZeroHom.snd_mono, Valuation.isClopen_ball, Valued.isOpen_closedBall, Valuation.hasBasis_nhds, Valued.mem_nhds_zero, Valued.isOpen_ball, Valued.mem_nhds, Valuation.isOpen_ball, exp_pos, addLeftMono, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero, IsValuativeTopology.isClosed_ball, LinearOrderedCommGroupWithZero.fst_apply, WithVal.valueGroupOrderIso₀_symm_restrict, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, Valuation.hasBasis_uniformity, WithZeroMulInt.toNNReal_strictMono, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, Valuation.restrict_le_one_iff, Valuation.isClosed_ball, OrderIso.withZeroUnits_apply, Valuation.IsEquiv.orderMonoidIso_eq_refl, MonoidWithZeroHom.inr_strictMono, Valued.hasBasis_uniformity, ValuativeRel.valuation_lt_symm_orderMonoidIso, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, Valuation.restrict_lt_iff, Padic.norm_rat_le_one_iff_padicValuation_le_one, Valued.isClosed_closedBall, Set.integer_valuation_le_one, Valuation.isOpen_closedBall, MonoidWithZeroHom.inl_mono, denselyOrdered_iff, not_denselyOrdered_withZero_int, instMulPosStrictMonoWithZeroOfMulRightStrictMono, toMulBot_le, ValuativeRel.restrict_lt_orderMonoidIso, Int.padicValuation_le_one, LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono, WeierstrassCurve.HasMultiplicativeReduction.badReduction, Valuation.IsEquiv.orderMonoidIso_spec, log_lt_iff_lt_exp, LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered, Valued.isClopen_closedBall, LinearOrderedCommGroupWithZero.inl_apply, LinearOrderedCommGroupWithZero.inr_apply, total_le, MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid, instPosMulStrictMonoWithZeroOfMulLeftStrictMono, Valued.exists_pow_lt_of_le_exp_neg_one, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, Valuation.RankLeOne.strictMono', Valuation.exists_setOf_restrict_le_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono, min_le_iff, le_exp_log, val_logOrderIso_symm_apply, instWellFoundedGTWithZeroMultiplicativeIntLeOne, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero, MonoidWithZeroHom.ValueGroup₀.embedding_strictMono, instCanonicallyOrderedAdd, toMulBot_strictMono, val_inv_logOrderIso_symm_apply, IsValuativeTopology.isClopen_closedBall, Valuation.mem_nhds_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem, lt_ofAdd_of_toAdd_unzero_lt, Valuation.is_topological_valuation, Valuation.IsEquiv.orderMonoidIso_symm, withZeroUnitsEquiv_strictMono, LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered, Rat.padicValuation_le_one_iff, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers
le 📖	CompOp	13 math math: coe_le_iff, nonpos_iff_eq_zero, coe_le_one, le_def, unzero_le_unzero, zero_le, unbot_le_iff, le_unzero_iff, one_le_coe, le_coe_iff, coe_le_coe, not_coe_le_zero, IsMax.withZero
logOrderIso 📖	CompOp	3 math math: logOrderIso_apply, val_logOrderIso_symm_apply, val_inv_logOrderIso_symm_apply
semilatticeInf 📖	CompOp	2 math math: coe_inf, min_le_iff
semilatticeSup 📖	CompOp	4 math math: FunctionField.InftyValuation.map_add_le_max', coe_sup, IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max', le_max_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addLeftMono 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero	AddLeftMono WithZero instAdd AddZero.toAdd AddZeroClass.toAddZero Preorder.toLE instPreorder	—	zero_add add_zero le_refl coe_add coe_le_coe le_add_of_nonneg_right coe_le_iff add_le_add_right
coe_inf 📖	mathematical	—	coe SemilatticeInf.toMin WithZero semilatticeInf	—	—
coe_le_coe 📖	mathematical	—	WithZero le coe	—	WithBot.coe_le_coe
coe_le_iff 📖	mathematical	—	WithZero le coe	—	WithBot.coe_le_iff
coe_le_one 📖	mathematical	—	WithZero le coe one	—	coe_le_coe
coe_lt_coe 📖	mathematical	—	WithZero instLT coe	—	—
coe_lt_one 📖	mathematical	—	WithZero instLT coe one	—	coe_lt_coe
coe_sup 📖	mathematical	—	coe SemilatticeSup.toMax WithZero semilatticeSup	—	—
exists_ne_zero_and_le_and_le 📖	mathematical	—	WithZero Preorder.toLE instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—
exists_ne_zero_and_lt 📖	mathematical	—	WithZero Preorder.toLT instPreorder	—	NoMinOrder.exists_lt coe_ne_zero coe_unzero coe_lt_coe
exists_ne_zero_and_lt_and_lt 📖	mathematical	—	WithZero Preorder.toLT instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_ne_zero_and_le_and_le exists_ne_zero_and_lt lt_of_lt_of_le
expOrderIso_symm_apply 📖	mathematical	—	DFunLike.coe RelIso Units WithZero Multiplicative MonoidWithZero.toMonoid instMonoidWithZero Multiplicative.monoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Preorder.toLE Units.instPreorder instPreorder Multiplicative.preorder RelIso.instFunLike RelIso.symm expOrderIso Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd unzero Units.val DivInvMonoid.toMonoid Group.toDivInvMonoid Multiplicative.group	—	—
exp_le_exp 📖	mathematical	—	WithZero Multiplicative Preorder.toLE instPreorder Multiplicative.preorder exp	—	—
exp_lt_exp 📖	mathematical	—	WithZero Multiplicative Preorder.toLT instPreorder Multiplicative.preorder exp	—	—
exp_pos 📖	mathematical	—	WithZero Multiplicative Preorder.toLT instPreorder Multiplicative.preorder instZero exp	—	—
instCanonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd WithZero instAdd AddZero.toAdd AddZeroClass.toAddZero Preorder.toLE instPreorder	—	instExistsAddOfLE CanonicallyOrderedAdd.toExistsAddOfLE bot_le le_rfl coe_le_coe le_add_self le_self_add
instExistsAddOfLE 📖	mathematical	—	ExistsAddOfLE WithZero instAdd Preorder.toLE instPreorder	—	zero_add instIsEmptyFalse ExistsAddOfLE.exists_add_of_le coe_le_coe
instMulLeftMono 📖	mathematical	—	MulLeftMono WithZero MulZeroClass.toMul instMulZeroClass Preorder.toLE instPreorder	—	zero_le coe_le_iff coe_mul coe_le_coe mul_le_mul_right
instMulLeftReflectLT 📖	mathematical	—	MulLeftReflectLT WithZero MulZeroClass.toMul instMulZeroClass Preorder.toLT instPreorder PartialOrder.toPreorder	—	LT.lt.ne' LE.le.trans_lt zero_le MulZeroClass.zero_mul MulZeroClass.mul_zero zero_lt_coe coe_lt_coe lt_of_mul_lt_mul_left'
isOrderedAddMonoid 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	IsOrderedAddMonoid WithZero instAddCommMonoid AddCommMonoid.toAddCommSemigroup instPreorder PartialOrder.toPreorder	—	addLeftMono IsOrderedAddMonoid.toAddLeftMono add_le_add_left covariant_swap_add_of_covariant_add add_comm
isOrderedMonoid 📖	mathematical	—	IsOrderedMonoid WithZero CommMonoidWithZero.toCommMonoid instCommMonoidWithZero instPreorder	—	mul_le_mul_left covariant_swap_mul_of_covariant_mul instMulLeftMono IsOrderedMonoid.toMulLeftMono
le_coe_iff 📖	mathematical	—	WithZero le coe	—	WithBot.le_coe_iff
le_def 📖	mathematical	—	WithZero le coe	—	WithBot.le_iff_forall
le_exp_log 📖	mathematical	—	WithZero Multiplicative Preorder.toLE instPreorder Multiplicative.preorder exp log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	le_refl
le_exp_of_log_le 📖	mathematical	Preorder.toLE log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	WithZero Multiplicative Preorder.toLE instPreorder Multiplicative.preorder exp	—	eq_or_ne
le_log_iff_exp_le 📖	mathematical	—	Preorder.toLE log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid WithZero Multiplicative instPreorder Multiplicative.preorder exp	—	CanLift.prf instCanLift
le_log_of_exp_le 📖	mathematical	WithZero Multiplicative Preorder.toLE instPreorder Multiplicative.preorder exp	Preorder.toLE log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	le_log_iff_exp_le LT.lt.ne' LT.lt.trans_le exp_pos
le_max_iff 📖	mathematical	—	WithZero Preorder.toLE instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder coe SemilatticeSup.toMax semilatticeSup Lattice.toSemilatticeSup	—	—
le_ofAdd_iff 📖	mathematical	—	WithZero Multiplicative Preorder.toLE instPreorder Multiplicative.preorder coe DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd Multiplicative.toAdd unzero	—	toAdd_unzero_le_of_lt_ofAdd le_ofAdd_of_toAdd_unzero_le
le_ofAdd_of_toAdd_unzero_le 📖	mathematical	Preorder.toLE DFunLike.coe Equiv Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd unzero	WithZero Multiplicative Preorder.toLE instPreorder Multiplicative.preorder coe DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	coe_unzero coe_le_coe ofAdd_toAdd Multiplicative.ofAdd_le
le_unzero_iff 📖	mathematical	—	unzero WithZero le coe	—	WithBot.le_unbot_iff
logOrderIso_apply 📖	mathematical	—	DFunLike.coe RelIso Units WithZero Multiplicative MonoidWithZero.toMonoid instMonoidWithZero Multiplicative.monoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Preorder.toLE Units.instPreorder instPreorder Multiplicative.preorder RelIso.instFunLike logOrderIso Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd unzero Units.val DivInvMonoid.toMonoid Group.toDivInvMonoid Multiplicative.group	—	—
log_le_iff_le_exp 📖	mathematical	—	Preorder.toLE log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid WithZero Multiplicative instPreorder Multiplicative.preorder exp	—	CanLift.prf instCanLift
log_le_log 📖	mathematical	—	Preorder.toLE log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid WithZero Multiplicative instPreorder Multiplicative.preorder	—	CanLift.prf instCanLift
log_lt_iff_lt_exp 📖	mathematical	—	Preorder.toLT log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid WithZero Multiplicative instPreorder Multiplicative.preorder exp	—	CanLift.prf instCanLift
log_lt_log 📖	mathematical	—	Preorder.toLT log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid WithZero Multiplicative instPreorder Multiplicative.preorder	—	CanLift.prf instCanLift
lt_coe_iff 📖	mathematical	—	WithZero instLT coe	—	WithBot.lt_coe_iff
lt_def 📖	mathematical	—	WithZero instLT instZero coe	—	WithBot.lt_def
lt_exp_of_log_lt 📖	mathematical	Preorder.toLT log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	WithZero Multiplicative Preorder.toLT instPreorder Multiplicative.preorder exp	—	eq_or_ne
lt_iff_exists 📖	mathematical	—	WithZero instLT coe	—	WithBot.lt_iff_exists
lt_iff_exists_coe 📖	mathematical	—	WithZero instLT coe	—	WithBot.lt_iff_exists_coe
lt_log_iff_exp_lt 📖	mathematical	—	Preorder.toLT log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid WithZero Multiplicative instPreorder Multiplicative.preorder exp	—	CanLift.prf instCanLift
lt_log_of_exp_lt 📖	mathematical	WithZero Multiplicative Preorder.toLT instPreorder Multiplicative.preorder exp	Preorder.toLT log SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	lt_log_iff_exp_lt LT.lt.ne' LT.lt.trans exp_pos
lt_mul_exp_iff_le 📖	mathematical	—	WithZero Multiplicative Preorder.toLT instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toMul instMulZeroClass Multiplicative.mul exp Preorder.toLE	—	CanLift.prf instCanLift eq_or_ne LinearOrderedCommMonoidWithZero.toPosMulStrictMono Multiplicative.isOrderedCancelMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid Int.instIsOrderedAddMonoid PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE log_le_log log_lt_log instNoZeroDivisors log_mul
lt_ofAdd_iff 📖	mathematical	—	WithZero Multiplicative Preorder.toLT instPreorder Multiplicative.preorder coe DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd Multiplicative.toAdd unzero	—	toAdd_unzero_lt_of_lt_ofAdd lt_ofAdd_of_toAdd_unzero_lt
lt_ofAdd_of_toAdd_unzero_lt 📖	mathematical	Preorder.toLT DFunLike.coe Equiv Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd unzero	WithZero Multiplicative Preorder.toLT instPreorder Multiplicative.preorder coe DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	coe_unzero coe_lt_coe ofAdd_toAdd Multiplicative.ofAdd_lt
lt_unzero_iff 📖	mathematical	—	unzero WithZero instLT coe	—	WithBot.lt_unbot_iff
map'_mono 📖	mathematical	Monotone DFunLike.coe MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike	Monotone WithZero instPreorder DFunLike.coe MonoidWithZeroHom instMulZeroOneClass MonoidWithZeroHom.funLike map'	—	map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass
map'_strictMono 📖	mathematical	StrictMono DFunLike.coe MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike	StrictMono WithZero instPreorder DFunLike.coe MonoidWithZeroHom instMulZeroOneClass MonoidWithZeroHom.funLike map'	—	map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass
min_le_iff 📖	mathematical	—	WithZero Preorder.toLE instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin semilatticeInf coe	—	—
nonpos_iff_eq_zero 📖	mathematical	—	WithZero le instZero	—	WithBot.le_bot_iff
not_coe_le_zero 📖	mathematical	—	WithZero le coe instZero	—	WithBot.not_coe_le_bot
not_lt_zero 📖	mathematical	—	WithZero instLT instZero	—	—
one_le_coe 📖	mathematical	—	WithZero le one coe	—	coe_le_coe
one_lt_coe 📖	mathematical	—	WithZero instLT one coe	—	coe_lt_coe
pos_iff_ne_zero 📖	mathematical	—	WithZero instLT instZero	—	WithBot.bot_lt_iff_ne_bot
toAdd_unzero_le_of_lt_ofAdd 📖	mathematical	WithZero Multiplicative Preorder.toLE instPreorder Multiplicative.preorder coe DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	Preorder.toLE DFunLike.coe Equiv Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd unzero	—	toAdd_ofAdd Multiplicative.toAdd_le coe_le_coe coe_unzero
toAdd_unzero_lt_of_lt_ofAdd 📖	mathematical	WithZero Multiplicative Preorder.toLT instPreorder Multiplicative.preorder coe DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	Preorder.toLT DFunLike.coe Equiv Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd unzero	—	toAdd_ofAdd Multiplicative.toAdd_lt coe_lt_coe coe_unzero
total_le 📖	mathematical	—	WithZero Preorder.toLE instPreorder	—	instReflLe
unbot_le_iff 📖	mathematical	—	unzero WithZero le coe	—	WithBot.unbot_le_iff
unzero_le_unzero 📖	mathematical	—	unzero WithZero le	—	WithBot.unbot_le_unbot_iff
unzero_lt_iff 📖	mathematical	—	unzero WithZero instLT coe	—	WithBot.unbot_lt_iff
val_expOrderIso_apply 📖	mathematical	—	Units.val WithZero Multiplicative MonoidWithZero.toMonoid instMonoidWithZero Multiplicative.monoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DFunLike.coe RelIso Units Preorder.toLE Units.instPreorder instPreorder Multiplicative.preorder RelIso.instFunLike expOrderIso coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	—
val_inv_expOrderIso_apply 📖	mathematical	—	Units.val WithZero Multiplicative MonoidWithZero.toMonoid instMonoidWithZero Multiplicative.monoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Units Units.instInv DFunLike.coe RelIso Preorder.toLE Units.instPreorder instPreorder Multiplicative.preorder RelIso.instFunLike expOrderIso InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid instGroupWithZero Multiplicative.group coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	—
val_inv_logOrderIso_symm_apply 📖	mathematical	—	Units.val WithZero Multiplicative MonoidWithZero.toMonoid instMonoidWithZero DivInvMonoid.toMonoid Group.toDivInvMonoid Multiplicative.group Units Units.instInv DFunLike.coe RelIso Multiplicative.monoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Preorder.toLE Units.instPreorder instPreorder Multiplicative.preorder RelIso.instFunLike RelIso.symm logOrderIso InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid instGroupWithZero coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	—
val_logOrderIso_symm_apply 📖	mathematical	—	Units.val WithZero Multiplicative MonoidWithZero.toMonoid instMonoidWithZero DivInvMonoid.toMonoid Group.toDivInvMonoid Multiplicative.group DFunLike.coe RelIso Units Multiplicative.monoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Preorder.toLE Units.instPreorder instPreorder Multiplicative.preorder RelIso.instFunLike RelIso.symm logOrderIso coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	—
zero_eq_bot 📖	mathematical	—	WithZero instZero Bot.bot instBot	—	—
zero_le 📖	mathematical	—	WithZero le instZero	—	bot_le
zero_lt_coe 📖	mathematical	—	WithZero instLT instZero coe	—	—

(root)

Definitions

Name	Category	Theorems
LinearOrderedCommGroupWithZero 📖	CompData	—
LinearOrderedCommMonoidWithZero 📖	CompData	—
instLinearOrderedAddCommGroupWithTopAdditiveOrderDual 📖	CompOp	—
instLinearOrderedAddCommGroupWithTopOrderDualAdditive 📖	CompOp	—
instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual 📖	CompOp	—
instLinearOrderedAddCommMonoidWithTopOrderDualAdditive 📖	CompOp	6 math math: Valuation.ofAddValuation_apply, Valuation.toAddValuation_apply, Valuation.ofAddValuation_toAddValuation, Valuation.toAddValuation_symm_eq, Valuation.toValuation_ofValuation, Valuation.ofAddValuation_symm_eq
instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop 📖	CompOp	11 math math: ArchimedeanClass.FiniteResidueField.mk_eq_zero, ArchimedeanClass.FiniteElement.val_add, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, ArchimedeanClass.FiniteElement.val_mul, ArchimedeanClass.FiniteElement.val_sub, ArchimedeanClass.FiniteResidueField.mk_eq_mk, ArchimedeanClass.FiniteElement.val_zero, ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, ArchimedeanClass.FiniteResidueField.mk_ne_zero, ArchimedeanClass.FiniteElement.val_one, ArchimedeanClass.FiniteElement.ext_iff
instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual 📖	CompOp	22 math math: ofDual_toAdd_zero, ArchimedeanClass.FiniteResidueField.mk_eq_zero, ArchimedeanClass.FiniteElement.val_add, AddValuation.toValuation_ofValuation, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, ofAdd_bot, ArchimedeanClass.FiniteElement.val_mul, ArchimedeanClass.FiniteElement.val_sub, ArchimedeanClass.FiniteResidueField.mk_eq_mk, AddValuation.ofValuation_toValuation, ArchimedeanClass.FiniteElement.val_zero, ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, ArchimedeanClass.FiniteResidueField.mk_ne_zero, ArchimedeanClass.FiniteElement.val_one, ofDual_toAdd_eq_top_iff, AddValuation.toValuation_apply, AddValuation.toValuation_symm_eq, AddValuation.ofValuation_symm_eq, ofAdd_toDual_eq_zero_iff, AddValuation.supp_quot_supp, AddValuation.ofValuation_apply, ArchimedeanClass.FiniteElement.ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_eq_zero'' 📖	mathematical	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommMonoidWithZero.toOrderBot MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	eq_of_forall_ge_iff
denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units 📖	mathematical	—	DenselyOrdered Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Nontrivial Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Units.instPreorder	—	exists_between zero_lt_one' LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one GroupWithZero.toNontrivial LT.lt.ne' LT.lt.ne Units.val_lt_val ne_zero_of_lt CanLift.prf instCanLiftUnitsValIsUnit Ne.isUnit LE.le.eq_or_lt zero_le' exists_one_lt' Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid Units.val_inv_eq_inv_val LinearOrderedCommMonoidWithZero.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toIsOrderedCancelMonoid IsOrderedMonoid.toMulLeftMono contravariant_lt_of_covariant_le DenselyOrdered.dense
denselyOrdered_units_iff 📖	mathematical	—	DenselyOrdered Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Preorder.toLT Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	—	denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units
instDenselyOrderedUnits 📖	mathematical	—	DenselyOrdered Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Preorder.toLT Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	—	denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units
instIsCancelMulZero_1 📖	mathematical	—	IsCancelMulZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero MulZeroClass.toZero	—	StrictMono.injective strictMono_mul_left_of_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono zero_lt_iff strictMono_mul_right_of_pos LinearOrderedCommMonoidWithZero.toMulPosStrictMono
instNontrivialUnitsOfDenselyOrdered 📖	mathematical	—	Nontrivial Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units
inv_mul_lt_of_lt_mul₀ 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid	—	mul_comm mul_inv_lt_of_lt_mul₀
le_zero_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	—
lt_of_mul_lt_mul_of_le₀ 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MulZeroClass.toZero Preorder.toLE	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	—	ne_of_gt lt_of_lt_of_le inv_mul_cancel_left₀ LT.lt.ne' mul_lt_mul_of_le_of_lt_of_nonneg_of_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono MulPosStrictMono.toMulPosMono LinearOrderedCommMonoidWithZero.toMulPosStrictMono inv_le_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE zero_lt_iff zero_le' inv_pos
mul_inv_lt_of_lt_mul₀ 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid	—	Mathlib.Tactic.Contrapose.contrapose₁ inv_inv mul_inv_le_of_le_mul₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono zero_le'
ne_zero_of_lt 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder	—	—	not_lt_zero'
not_lt_zero' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	LE.le.not_gt zero_le'
ofAdd_bot 📖	mathematical	—	DFunLike.coe Equiv OrderDual Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd Bot.bot OrderDual.instBotOfTop OrderTop.toTop Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder LinearOrderedAddCommMonoidWithTop.toOrderTop MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual	—	—
ofAdd_toDual_eq_zero_iff 📖	mathematical	—	DFunLike.coe Equiv OrderDual Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd OrderDual.toDual MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder LinearOrderedAddCommMonoidWithTop.toOrderTop	—	—
ofDual_toAdd_eq_top_iff 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual Multiplicative Multiplicative.toAdd Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder LinearOrderedAddCommMonoidWithTop.toOrderTop MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual	—	—
ofDual_toAdd_zero 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual Multiplicative Multiplicative.toAdd MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrderedAddCommMonoidWithTop.toLinearOrder LinearOrderedAddCommMonoidWithTop.toOrderTop	—	—
pow_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 Monoid.toPow MonoidWithZero.toMonoid	—	pow_ne_zero_iff isReduced_of_noZeroDivisors
zero_le' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	LinearOrderedCommMonoidWithZero.zero_le
zero_lt_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	—	—

---

← Back to Index