WithZero

📁 Source: Mathlib/Data/Int/WithZero.lean

Statistics

Metric	Count
Definitions WithZero, toNNReal	2
Theorems toNNReal_eq_one_iff, toNNReal_le_one_iff, toNNReal_lt_one_iff, toNNReal_ne_zero, toNNReal_neg_apply, toNNReal_pos, toNNReal_pos_apply, toNNReal_strictMono	8
Total	10

WithZeroMulInt

Definitions

Name	Category	Theorems
toNNReal 📖	CompOp	11 math math: NumberField.FinitePlace.norm_def', toNNReal_pos, toNNReal_lt_one_iff, toNNReal_neg_apply, toNNReal_le_one_iff, NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, NumberField.FinitePlace.norm_def_int, toNNReal_eq_one_iff, toNNReal_strictMono, NumberField.toNNReal_valued_eq_adicAbv, toNNReal_pos_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNNReal_eq_one_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom WithZero Multiplicative NNReal WithZero.instMulZeroOneClass Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidWithZeroHom.funLike toNNReal instOneNNReal WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass NeZero.charZero_one IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing NeZero.one WithZero.instNontrivial WithZero.coe_unzero toAdd_eq_zero zpow_eq_one_iff_right₀ LinearOrderedCommMonoidWithZero.toPosMulStrictMono LinearOrderedCommMonoidWithZero.toZeroLeOneClass zero_le NNReal.instCanonicallyOrderedAdd toNNReal_neg_apply WithZero.coe_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
toNNReal_le_one_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	Preorder.toLE DFunLike.coe MonoidWithZeroHom WithZero Multiplicative WithZero.instMulZeroOneClass Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidWithZeroHom.funLike toNNReal ne_zero_of_lt LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero NNReal.instLinearOrderedCommGroupWithZero WithZero.instPreorder Multiplicative.preorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	ne_zero_of_lt StrictMono.le_iff_le toNNReal_strictMono map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass
toNNReal_lt_one_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	DFunLike.coe MonoidWithZeroHom WithZero Multiplicative WithZero.instMulZeroOneClass Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidWithZeroHom.funLike toNNReal ne_zero_of_lt LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero NNReal.instLinearOrderedCommGroupWithZero WithZero.instPreorder Multiplicative.preorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	ne_zero_of_lt StrictMono.lt_iff_lt toNNReal_strictMono map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass
toNNReal_ne_zero 📖	—	—	—	—	MonoidWithZeroHom.monoidWithZeroHomClass
toNNReal_neg_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom WithZero Multiplicative NNReal WithZero.instMulZeroOneClass Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidWithZeroHom.funLike toNNReal NNReal.zpow Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd WithZero.unzero	—	—
toNNReal_pos 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal DFunLike.coe MonoidWithZeroHom WithZero Multiplicative WithZero.instMulZeroOneClass Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidWithZeroHom.funLike toNNReal	—	lt_of_le_of_ne zero_le' toNNReal_ne_zero
toNNReal_pos_apply 📖	mathematical	WithZero Multiplicative WithZero.instZero	DFunLike.coe MonoidWithZeroHom NNReal WithZero.instMulZeroOneClass Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidWithZeroHom.funLike toNNReal instZeroNNReal	—	—
toNNReal_strictMono 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	StrictMono WithZero Multiplicative WithZero.instPreorder Multiplicative.preorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe MonoidWithZeroHom WithZero.instMulZeroOneClass Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiringNNReal MonoidWithZeroHom.funLike toNNReal ne_zero_of_lt LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero NNReal.instLinearOrderedCommGroupWithZero	—	ne_zero_of_lt Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono LinearOrderedCommMonoidWithZero.toZeroLeOneClass LT.lt.bot_lt zpow_lt_zpow_iff_right₀ Multiplicative.toAdd_lt WithZero.coe_lt_coe WithZero.coe_unzero

(root)

Definitions

Name	Category	Theorems
WithZero 📖	CompOp	406 math math: WithZero.instNontrivial, WithZero.unzero_mul, WithZero.logOrderIso_apply, WithZero.exp_add, WithZero.instExistsAddOfLE, IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', OrderMonoidIso.val_inv_unitsWithZero_symm_apply, WithZero.val_expOrderIso_apply, WithZero.logEquiv_symm, instPosMulMonoWithZeroOfMulLeftMono, ValuationSubring.integralClosure_algebraMap_injective, WithZero.map'_mono, NumberField.prod_nonarchAbsVal_eq, WithZero.map'_zero, NumberField.FinitePlace.mk_apply, WithZero.isOrderedMonoid, MonoidWithZeroHom.snd_comp_inl, WithZero.mulArchimedean_iff, Padic.withValUniformEquiv_norm_le_one_iff, WithZero.withZeroUnitsEquiv_symm_apply_coe, Rat.padicValuation_cast, WithZero.map'_coe, WithZero.recZeroCoe_one, WithZero.mapAddHom_comp, WithZero.coe_unitsWithZeroEquiv_eq_units_val, WithZero.lift'_symm_apply_apply, LaurentSeries.LaurentSeriesRingEquiv_def, Ring.ordFrac_eq_div, OrderMonoidIso.withZero_symm_apply_symm_apply, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, OrderMonoidIso.withZero_symm_apply_apply, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, Set.unit_eq, Padic.instCompatibleWithZeroMultiplicativeIntMulValuation, NumberField.FinitePlace.norm_def', IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, FunctionField.inftyValuation.X_inv, Int.padicValuation_lt_one_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, NumberField.FinitePlace.embedding_apply, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, LaurentSeries.valuation_single_zpow, WithZero.exp_lt_exp, WithZero.log_le_log, IsDedekindDomain.HeightOneSpectrum.intValuation_le_one, WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral, WithZero.zero_eq_bot, FunctionField.InftyValuation.map_zero', WithZero.coe_le_iff, WithZero.lt_iff_exists, WithZero.coe_zpow, IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntValuation, WithZero.map'_strictMono, WithZero.exp_sub, Int.padicValuation_eq_one_iff, Ring.ordFrac_eq_ord, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem, WithZero.coe_expEquiv_apply, IsDedekindDomain.HeightOneSpectrum.intValuation_singleton, MonoidWithZeroHom.fst_mono, FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation, Rat.padicValuation_self, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', WithZero.recZeroCoe_zero, WithZero.isOrderedAddMonoid, WithZero.log_inv, NumberField.FinitePlace.norm_embedding_eq, Polynomial.valuation_of_mk, WithZero.mapAddHom_id, WithZero.log_le_iff_le_exp, WithZero.expOrderIso_symm_apply, ValuativeRel.nonempty_orderIso_withZeroMul_int_iff, LaurentSeries.inducing_coe, AddEquiv.withZeroCongr_apply, LaurentSeries.continuous_coe, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, WithZero.lt_ofAdd_iff, Padic.norm_eq_zpow_log_mulValuation, PowerSeries.intValuation_eq_of_coe, WithZeroMulInt.toNNReal_pos, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, LaurentSeries.val_le_one_iff_eq_coe, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer, IsDiscreteValuationRing.isRankOneDiscrete, instIsCyclicUnitsWithZero, WithZero.coe_div, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, MulEquiv.withZero_apply_symm_apply, WithZero.lt_iff_exists_coe, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, WithZero.lt_mul_exp_iff_le, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, OrderMonoidIso.withZeroUnits_symm_apply, FunctionField.valuedFqtInfty.def, MonoidWithZeroHom.inl_strictMono, WithZero.expEquiv_symm, WithZeroMulInt.toNNReal_lt_one_iff, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, OrderMonoidIso.withZeroUnits_apply, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, AddEquiv.withZeroCongr_symm, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, IsDedekindDomain.HeightOneSpectrum.valuation_def, WithZero.lift'_coe, WithZero.log_one, OrderMonoidIso.val_unitsWithZero_symm_apply, IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero', OrderIso.withZeroUnits_symm_apply, WithZero.map'_surjective, FunctionField.InftyValuation.map_add_le_max', WeierstrassCurve.IsMinimal.val_Δ_maximal, LaurentSeries.exists_ratFunc_val_lt, MulEquiv.withZero_apply_apply, WithZero.instNontrivialUnits, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, Padic.mulValuation_toFun, WithZero.coe_sup, WithZero.coe_inv, IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff, WithZero.instNoZeroDivisors, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd, WithZero.withZeroUnitsEquiv_symm_strictMono, WithZero.map₂_eq_bot_iff, IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max', WithZero.pos_iff_ne_zero, Padic.comap_mulValuation_eq_padicValuation, OrderMonoidIso.withZero_apply_symm_apply, WithZero.map₂_bot_left, WithZero.coe_pow, NumberField.FinitePlace.norm_lt_one_iff_mem, WithZeroMulInt.toNNReal_neg_apply, Rat.valuation_le_one_iff_den, WithZero.exp_eq_one, WithZero.unitsWithZeroEquiv_symm_apply, WithZero.nonpos_iff_eq_zero, WithZero.le_max_iff, WithZero.map_id, WeierstrassCurve.isGoodReduction_iff, WithZero.map'_injective, WithZero.monoidWithZeroHom_ext_iff, WithZero.coe_le_one, LaurentSeries.exists_Polynomial_intValuation_lt, WithZero.exp_le_exp, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', WithZero.toMulBot_lt, MonoidWithZeroHom.fst_comp_inl, WithZero.coe_neg, ValuationSubring.instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt, WithZero.log_div, WithZero.exists_ne_zero_and_le_and_le, instDenselyOrderedWithZeroOfNoMinOrder, WithZero.le_def, WithZero.lift_coe, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, WithZero.exists_ne_zero_and_lt_and_lt, WithZero.log_pow, WithZero.mapAddHom_injective', WithZero.instLeftDistribClass, WithZero.unzero_le_unzero, LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ, OrderMonoidIso.unitsWithZero_apply, WithZeroMulInt.toNNReal_le_one_iff, WithZero.val_inv_expOrderIso_apply, FunctionField.InftyValuation.map_one', IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', WithZero.exists_ne_zero_and_lt, WithZero.log_lt_log, RatFunc.valuation_eq_LaurentSeries_valuation, WithZero.log_mul, PadicInt.coe_adicCompletionIntegersEquiv_apply, WithZero.map_bot, NumberField.isFinitePlace_iff, MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit, OrderMonoidIso.withZero_apply_apply, WithZero.toMulBot_coe_ofAdd, WithZero.log_zpow, WithZero.le_exp_of_log_le, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, LaurentSeries.coe_X_compare, FunctionField.InftyValuation.map_mul', WithZero.instMulLeftMono, WithZero.coe_inf, NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, WithZero.lift'_unique, WithZero.mapAddHom_coe, AddEquiv.withZeroCongr_refl, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, NumberField.FinitePlace.coe_apply, Int.padicValuation_self, WithZero.le_ofAdd_of_toAdd_unzero_le, IsDedekindDomain.HeightOneSpectrum.intValuation.map_one', WithZero.exists, WithZero.zero_le, WithZero.le_log_iff_exp_le, WithZero.instRightDistribClass, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, NumberField.FinitePlace.norm_def_int, WithZero.one_lt_coe, MonoidWithZeroHom.inr_mono, WithZero.unbot_le_iff, WithZero.not_lt_zero, WithZero.coe_lt_one, AddEquiv.withZeroCongr_trans, WithZero.instMulLeftReflectLT, WithZero.lt_unzero_iff, WithZero.exp_nsmul, ValuationSubring.isIntegral_of_mem_ringOfIntegers', WithZero.lt_exp_of_log_lt, MonoidWithZeroHom.snd_inr, MonoidWithZeroHom.snd_inl_apply_of_ne_zero, WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd, WithZero.toMulBot_zero, WithZero.denselyOrdered_set_iff_subsingleton, WithZero.lift_zero, IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring, MonoidWithZeroHom.inl_injective, WithZero.le_unzero_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, WithZero.instCanLiftMultiplicativeExpNeOfNat, LaurentSeries.valuation_LaurentSeries_equal_extension, WeierstrassCurve.isMinimal_iff, instMulPosMonoWithZeroOfMulRightMono, RatFunc.v_def, Rat.padicValuation_eq_zero_iff, LaurentSeries.LaurentSeries_coe, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff, LaurentSeries.powerSeries_ext_subring, Set.unit_valuation_eq_one, WithZero.map_injective, WithZero.le_ofAdd_iff, LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, WithZero.forall, FunctionField.inftyValuation.X_zpow, WithZero.lt_log_iff_exp_lt, WithZero.logEquiv_apply, AddMonCat.adjoinZero_obj_coe, LaurentSeries.powerSeriesRingEquiv_coe_apply, LinearOrderedCommGroupWithZero.fst_comp_inl, WithZero.map_injective', instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, WithZero.one_le_coe, IsDedekindDomain.HeightOneSpectrum.intValuation_def, FunctionField.inftyValuation.X, MonoidWithZeroHom.snd_mono, IsDedekindDomain.HeightOneSpectrum.intValuationDef_zero, FunctionField.inftyValuedFqt.def, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, MonoidWithZeroHom.fst_apply_coe, MonoidWithZeroHom.fst_inl, MonoidWithZeroHom.fst_surjective, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, WithZero.inv_zero, WithZeroMulInt.toNNReal_eq_one_iff, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq, MonoidWithZeroHom.snd_comp_inr, WithZero.toMulBot_coe, WithZero.lift'_surjective, WithZero.exp_pos, LaurentSeries.instLaurentSeriesComplete, IsDedekindDomain.HeightOneSpectrum.valuation_surjective, WithZero.addLeftMono, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero, Padic.withValUniformEquiv_cast_apply, LaurentSeries.valuation_coe_ratFunc, MonoidWithZeroHom.inr_apply_unit, Padic.coe_withValRingEquiv, Padic.comap_mulValuation_eq_int_padicValuation, LinearOrderedCommGroupWithZero.fst_apply, NumberField.FinitePlace.norm_eq_one_iff_notMem, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, WithZeroMulInt.toNNReal_strictMono, WithZero.map₂_bot_right, LaurentSeries.tendsto_valuation, WithZero.le_coe_iff, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, LaurentSeries.coe_range_dense, PowerSeries.intValuation_X, MonoidWithZeroHom.fst_inr_apply_of_ne_zero, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', OrderIso.withZeroUnits_apply, WithZero.exp_zsmul, WithZero.lift_unique, Padic.coe_withValRingEquiv_symm, WithZero.withZeroUnitsEquiv_symm_apply, LaurentSeries.comparePkg_eq_extension, NumberField.toNNReal_valued_eq_adicAbv, MonoidWithZeroHom.inr_strictMono, WithZero.map'_surjective_iff, LaurentSeries.valuation_def, FunctionField.inftyValuation.C, WithZero.log_zero, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, MulEquiv.withZero_symm_apply_apply, WithZero.coe_injective, Rat.HeightOneSpectrum.valuation_equiv_padicValuation, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, WithZero.zero_lt_coe, LaurentSeries.uniformContinuous_coeff, IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul', Padic.norm_rat_le_one_iff_padicValuation_le_one, Set.integer_valuation_le_one, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, Rat.surjective_padicValuation, MonoidWithZeroHom.inl_mono, NumberField.FinitePlace.isFinitePlace, WithZero.denselyOrdered_iff, WithZero.map'_comp, not_denselyOrdered_withZero_int, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos, instMulPosStrictMonoWithZeroOfMulRightStrictMono, IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer, WithZero.expRecOn_zero, WithZero.coe_le_coe, WithZero.toMulBot_le, WithZero.instMulArchimedean, WithZero.not_coe_le_zero, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, Set.integer_eq, WithZero.map_map, WithZero.withZeroUnitsEquiv_apply, WithZero.map_comp, Int.padicValuation_le_one, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, WithZero.lift'_zero, MonoidWithZeroHom.snd_apply_coe, LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono, NumberField.FinitePlace.norm_le_one, WithZero.unzero_lt_iff, WithZero.coe_lt_coe, WithZero.coe_one, LaurentSeries.mem_integers_of_powerSeries, WithZero.log_lt_iff_lt_exp, WeierstrassCurve.IsGoodReduction.goodReduction, LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, WithZero.lt_coe_iff, LinearOrderedCommGroupWithZero.inl_apply, LinearOrderedCommGroupWithZero.inr_apply, WithZero.total_le, ValuationSubring.algebraMap_injective, IsMax.withZero, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, WithZero.coe_mul, instPosMulStrictMonoWithZeroOfMulLeftStrictMono, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq, MonoidWithZeroHom.inr_injective, WithZero.min_le_iff, WithZero.map'_id, MonoidWithZeroHom.commute_inl_inr, MonoidWithZeroHom.fst_comp_inr, WithZero.coeAddHom_apply, FunctionField.inftyValuation_apply, WithZero.le_exp_log, WithZero.val_logOrderIso_symm_apply, WithZero.lt_def, WithZero.toMulBot_symm_bot, instWellFoundedGTWithZeroMultiplicativeIntLeOne, LaurentSeries.exists_ratFunc_eq_v, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero, Padic.isDenseInducing_cast_withVal, WithZero.mapAddHom_injective, WithZero.instCanonicallyOrderedAdd, WithZero.exp_zero, WithZero.toMulBot_strictMono, WithZero.logEquiv_unitsMk0, WithZero.val_inv_logOrderIso_symm_apply, WithZero.coeMonoidHom_apply, IsDedekindDomain.HeightOneSpectrum.intValuation_apply, LaurentSeries.valuation_X_pow, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem, Int.padicValuation_eq_zero_iff, WithZero.unitsWithZeroEquiv_apply, WithZero.lt_ofAdd_of_toAdd_unzero_lt, WithZero.mapAddHom_mapAddHom, NumberField.FinitePlace.norm_def, MonoidWithZeroHom.inl_apply_unit, MonoidWithZeroHom.snd_surjective, WithZero.withZeroUnitsEquiv_strictMono, LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered, WithZero.exp_neg, WithZero.coe_add, WithZero.instCanLift, Rat.padicValuation_le_one_iff, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, AddMonCat.adjoinZero_map, MulEquiv.withZero_symm_apply_symm_apply, Polynomial.valuation_X_eq_neg_one, WithZero.map'_injective_iff, WithZero.exp_injective, WithZero.map'_map'

---

← Back to Index