Multiplicative

📁 Source: Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicative.lean

Statistics

Metric	Count
Definitions Multiplicative	1
Theorems induction_on_coprime, induction_on_prime_power, multiplicative_of_coprime, multiplicative_prime_power, prime_pow_coprime_prod_of_coprime_insert	5
Total	6

UniqueFactorizationMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_on_coprime 📖	—	MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Monoid.toNatPow MonoidWithZero.toMonoid MulZeroClass.toMul	—	—	isUnit_of_dvd_unit Units.isUnit prod_normalizedFactors Multiset.map_id Finset.prod_multiset_map_count induction_on_prime_power prime_of_normalized_factor normalizedFactors_eq_of_dvd
induction_on_prime_power 📖	mathematical	Prime Monoid.toNatPow MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	Finset.prod CommMonoidWithZero.toCommMonoid	—	Finset.induction_on isUnit_one Finset.prod_insert prime_pow_coprime_prod_of_coprime_insert Finset.mem_insert_self Finset.mem_insert_of_mem
multiplicative_of_coprime 📖	—	MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul Monoid.toNatPow MonoidWithZero.toMonoid	—	—	MulZeroClass.zero_mul MulZeroClass.mul_zero mul_one isUnit_one multiplicative_prime_power prime_of_normalized_factor normalize_normalized_factor normalize_eq_normalize toIsCancelMulZero Irreducible.dvd_symm Prime.irreducible prod_normalizedFactors mul_right_comm Units.isUnit mul_assoc Multiset.map_id Finset.prod_multiset_map_count Finset.prod_subset Finset.subset_union_left Multiset.count_eq_zero_of_notMem pow_zero Finset.subset_union_right Finset.prod_mul_distrib Finset.prod_congr
multiplicative_prime_power 📖	mathematical	Prime MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Monoid.toNatPow MonoidWithZero.toMonoid	Finset.prod CommMonoidWithZero.toCommMonoid	—	Finset.induction_on mul_one isUnit_one Finset.mem_insert_self Finset.mem_insert_of_mem prime_pow_coprime_prod_of_coprime_insert Finset.prod_insert pow_add mul_assoc mul_left_comm
prime_pow_coprime_prod_of_coprime_insert 📖	mathematical	Finset Finset.instMembership Prime	IsRelPrime MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Monoid.toNatPow Finset.prod CommMonoidWithZero.toCommMonoid	—	Finset.mem_insert_self isRelPrime_iff_no_prime_factors pow_ne_zero isReduced_of_noZeroDivisors IsRightCancelMulZero.to_noZeroDivisors IsCancelMulZero.toIsRightCancelMulZero toIsCancelMulZero Prime.ne_zero Prime.dvd_of_dvd_pow Prime.exists_mem_multiset_dvd Multiset.mem_map dvd_trans Irreducible.dvd_symm Prime.irreducible Finset.mem_val Finset.mem_insert_of_mem

(root)

Definitions

Name	Category	Theorems
Multiplicative 📖	CompOp	584 math math: AddMonoidAlgebra.singleHom_apply, WithZero.logOrderIso_apply, WithZero.exp_add, Finsupp.mulHom_ext'_iff, AddMonoidAlgebra.lift_apply', AddChar.toMonoidHomEquiv_zero, ofDual_toAdd_zero, IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', ofAdd_multiset_prod, WithZero.val_expOrderIso_apply, Multiplicative.isIsIsometricVAdd'', AddMonoidAlgebra.algHom_ext'_iff, WithZero.logEquiv_symm, nndist_ofAdd, CircleDeg1Lift.translate_inv_apply, ValuationSubring.integralClosure_algebraMap_injective, zpowersMulHom_symm_apply, NumberField.prod_nonarchAbsVal_eq, AddEquiv.toMultiplicative_apply_symm_apply, AddMonoidHom.toMultiplicative_add, NumberField.FinitePlace.mk_apply, Cardinal.mk_multiplicative, Padic.withValUniformEquiv_norm_le_one_iff, Multiplicative.ofAdd_eq_top, AddMonoidHom.toMultiplicativeRight_apply_apply, Rat.padicValuation_cast, orderOf_ofAdd_eq_addOrderOf, Multiplicative.instNontrivial, AddMonCat.equivalence_functor_obj_coe, AddSubsemigroup.coe_toSubsemigroup_symm_apply, LaurentSeries.LaurentSeriesRingEquiv_def, Order.succ_toAdd, Multiplicative.toAdd_image_setMul, Ring.ordFrac_eq_div, IsCyclic.val_mulAutMulEquiv_apply, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, instWeaklyLocallyCompactSpaceMultiplicative, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, AddEquiv.toMultiplicativeRight_apply_apply, Set.unit_eq, AddEquiv.additiveMultiplicative_apply, Padic.instCompatibleWithZeroMultiplicativeIntMulValuation, NumberField.FinitePlace.norm_def', MulEquiv.piMultiplicative_apply, instDenselyOrderedMultiplicative, 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, norm_ofAdd, Multiplicative.ofAdd_le, AddConstMap.coe_addLeftHom_apply, 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, ArchimedeanClass.FiniteResidueField.mk_eq_zero, zpowersHom_symm_apply, FunctionField.InftyValuation.map_zero', autEquivZmod_symm_apply_natCast, FreeMonoid.countP_of, ofAdd_toAdd, MonoidHom.coe_toMultiplicative_range, IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntValuation, AddGrpCat.toGrp_obj_coe, AddMonoidAlgebra.lift_mapRangeRingHom_algebraMap, WithZero.exp_sub, Int.padicValuation_eq_one_iff, Order.succ_ofAdd, Ring.ordFrac_eq_ord, AddMonoidHom.coe_toMultiplicativeRight, Multiplicative.ofAdd_lt, AddSubmonoid.coe_toSubmonoid_apply, Multiplicative.ofAdd_image_setAdd, ofAdd_zero, AddMonoidAlgebra.divOfHom_apply_apply, uliftZPowersHom_symm_apply, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem, WithZero.coe_expEquiv_apply, toAdd_mul, IsDedekindDomain.HeightOneSpectrum.intValuation_singleton, AddSubsemigroup.coe_toSubsemigroup_apply, FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation, MulEquiv.prodMultiplicative_symm_apply, Rat.padicValuation_self, MulAutMultiplicative_symm_apply_apply, Polynomial.eval₂_ofFinsupp, Order.pred_ofAdd, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', isSquare_ofAdd_iff, instIsTopologicalGroupMultiplicativeOfIsTopologicalAddGroup, WithZero.log_inv, NumberField.FinitePlace.norm_embedding_eq, Polynomial.valuation_of_mk, SkewPolynomial.φ_iterate_apply, norm_toAdd, SkewPolynomial.monomial_def, zpowersHom_apply, powersHom_symm_apply, WithZero.log_le_iff_le_exp, AddChar.toMonoidHomEquiv_symm_apply, WithZero.expOrderIso_symm_apply, ValuativeRel.nonempty_orderIso_withZeroMul_int_iff, instContinuousInvMultiplicativeOfContinuousNeg, LaurentSeries.inducing_coe, MulAutMultiplicative_apply_apply, isAddRegular_toAdd, Multiplicative.ofAdd_eq_bot, LaurentSeries.continuous_coe, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, toAdd_multiset_sum, ArchimedeanClass.FiniteElement.val_add, AddEquiv.toMultiplicativeLeft_apply_symm_apply, ComplexShape.TensorSigns.ε'_succ, WithZero.lt_ofAdd_iff, continuous_toAdd, Padic.norm_eq_zpow_log_mulValuation, AddMonCat.equivalence_counitIso, PowerSeries.intValuation_eq_of_coe, WithZeroMulInt.toNNReal_pos, instTotallyDisconnectedSpaceMultiplicative, CommGroup.equiv_prod_multiplicative_zmod_of_finite, Subgroup.range_zpowersHom, uliftPowersHom_symm_apply, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, AddChar.coe_toMonoidHomEquiv, MulEquiv.prodMultiplicative_apply, CircleDeg1Lift.translate_iterate, LaurentSeries.val_le_one_iff_eq_coe, AddEquiv.toMultiplicativeRight_apply_symm_apply, AddMonoidAlgebra.of_apply, AddValuation.toValuation_ofValuation, zpowersMulHom_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, AddCommMonCat.equivalence_functor_map, IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer, IsDiscreteValuationRing.isRankOneDiscrete, AddMonoidHom.toMultiplicativeRight_symm_apply_apply, FreeAbelianGroup.liftAddEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, WithZero.lt_mul_exp_iff_le, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, Submonoid.closure_singleton_eq, MonoidHom.apply_mnat, FunctionField.valuedFqtInfty.def, dist_ofAdd, WithZero.expEquiv_symm, WithZeroMulInt.toNNReal_lt_one_iff, AddEquiv.toAdditive_toMultiplicative_symm_apply, instCompactSpaceMultiplicative, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, ofAdd_bot, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, AddGroup.fg_iff_mul_fg, Multiplicative.mulAction_isPretransitive, MvPolynomial.monomialOneHom_apply, IsDedekindDomain.HeightOneSpectrum.valuation_def, WithZero.log_one, AddMonoidAlgebra.ringHom_ext'_iff, MulAutMultiplicative_symm_apply_symm_apply, AddCommGrpCat.toCommGrp_obj_coe, ofAdd_list_prod, IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero', toAdd_zpow, AddMonoidAlgebra.lift_apply, FunctionField.InftyValuation.map_add_le_max', WeierstrassCurve.IsMinimal.val_Δ_maximal, SkewPolynomial.φ_def, Pi.mulSingle_multiplicativeOfAdd_eq, isRegular_ofAdd, LaurentSeries.exists_ratFunc_val_lt, ArchimedeanClass.FiniteElement.val_mul, Int.toAdd_pow, dist_toAdd, Multiplicative.ofAdd_symm_eq, AddMonoidHom.toMultiplicative_symm_apply_apply, isClosedMap_ofAdd, AddMonoidHom.coe_toMultiplicativeLeft, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, AddSubgroup.toSubgroup_closure, MonoidHom.toAdditiveLeft_apply_apply, Padic.mulValuation_toFun, IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff, IsCyclic.val_inv_mulAutMulEquiv_apply, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd, isOfFinOrder_ofAdd_iff, IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max', even_toAdd_iff, Padic.comap_mulValuation_eq_padicValuation, NumberField.FinitePlace.norm_lt_one_iff_mem, WithZeroMulInt.toNNReal_neg_apply, instSubsingletonMultiplicative, Subgroup.mem_toAddSubgroup', Rat.valuation_le_one_iff_den, WithZero.exp_eq_one, Nat.ofAdd_mul, ofAdd_image_zmultiples_eq_zpowers_ofAdd, AddSubmonoid.toSubmonoid_closure, autEquivZmod_symm_apply_intCast, WeierstrassCurve.isGoodReduction_iff, LaurentSeries.exists_Polynomial_intValuation_lt, Monoid.exponent_multiplicative, toAdd_pow, LinearOrderedCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete, WithZero.exp_le_exp, nhds_toAdd, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', WithZero.toMulBot_lt, ValuationSubring.instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt, WithZero.log_div, ArchimedeanClass.FiniteElement.val_sub, ZModModule.isPGroup_multiplicative, isClosedMap_toAdd, Subgroup.coe_toAddSubgroup_symm_apply, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, WithZero.log_pow, ofAdd_smul, Multiplicative.ofAdd_strictMono, MulEquiv.AddMonoid.End_apply, Multiplicative.instTwoUniqueProdsOfTwoUniqueSums, toAdd_eq_zero, WithZeroMulInt.toNNReal_le_one_iff, CoxeterSystem.lengthParity_comp_simple, Multiplicative.toAdd_eq_top, WithZero.val_inv_expOrderIso_apply, IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le, FreeMonoid.count_of, FunctionField.InftyValuation.map_one', IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', Multiplicative.isOrderedCancelMonoid, AddEquiv.toMultiplicativeLeft_symm_apply_symm_apply, edist_toAdd, WithZero.log_lt_log, isOpenMap_toAdd, AddChar.toMonoidHom_apply, RatFunc.valuation_eq_LaurentSeries_valuation, Multiplicative.toAdd_image_nsmul, WithZero.log_mul, AddMonoidHom.toMultiplicative_id, ofAdd_sum, MulEquiv.toMultiplicative_toAdditive_symm_apply, PadicInt.coe_adicCompletionIntegersEquiv_apply, toAdd_ofAdd, NumberField.isFinitePlace_iff, AddEquiv.toMultiplicativeRight_symm_apply_apply, nnnorm_ofAdd, Finsupp.prod_hom_add_index, WithZero.toMulBot_coe_ofAdd, WithZero.log_zpow, WithZero.le_exp_of_log_le, AddGrpCat.toGrp_map, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, toAdd_one, Multiplicative.toAdd_eq_bot, LaurentSeries.coe_X_compare, FunctionField.InftyValuation.map_mul', IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_eq, NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, AddMonoidAlgebra.lift_single, Group.fg_of_mul_group_fg, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, AddMonoidHom.coe_toMultiplicative', CircleDeg1Lift.translate_apply, LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete, AddMonoidAlgebra.lift_symm_apply, NumberField.FinitePlace.coe_apply, instInfiniteMultiplicative, MulEquiv.multiplicativeAdditive_apply, instLocallyCompactSpaceMultiplicative, Int.padicValuation_self, AddEquiv.toMultiplicative_apply_apply, IsDedekindDomain.HeightOneSpectrum.intValuation.map_one', instNoncompactSpaceMultiplicative, AddChar.toMonoidHomEquiv_symm_one, Multiplicative.isRightCancelMul, toAdd_vadd, MonoidHom.coe_toAdditiveLeft, WithZero.le_log_iff_exp_le, ArchimedeanClass.FiniteResidueField.mk_eq_mk, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, AddValuation.ofValuation_toValuation, NumberField.FinitePlace.norm_def_int, Multiplicative.ofAdd_bot, FreeCommRing.of_cons, Multiplicative.mem_toSubgroup, WithZero.exp_nsmul, ValuationSubring.isIntegral_of_mem_ringOfIntegers', AddMonoidAlgebra.lift_of, powersHom_apply, ofAdd_add, AddMonoidHom.coe_toMultiplicative, instIsPredArchimedeanMultiplicative, WithZero.lt_exp_of_log_lt, CommGroup.equiv_free_prod_prod_multiplicative_zmod, powersMulHom_apply, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd, instIsKleinFourMultiplicativeOfIsAddKleinFour, ArchimedeanClass.FiniteElement.val_zero, Multiplicative.canonicallyOrderedMul, WithZero.toMulBot_zero, AddMonoidAlgebra.nonUnitalAlgHom_ext'_iff, CircleDeg1Lift.translate_zpow, Multiplicative.isIsometricSMul', Multiplicative.toAdd_lt, IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring, MonoidHom.toAdditiveRight_symm_apply_apply, AddMonoidHom.toMultiplicativeLeft_symm_apply_apply, instLipschitzMulMultiplicativeOfLipschitzAdd, Int.ofAdd_mul, ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, isAddLeftRegular_toAdd, Multiplicative.toAdd_symm_eq, Multiplicative.instMulArchimedean, IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, AddChar.toMonoidHomEquiv_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, MonoidHom.apply_mint, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, AddEquiv.toMultiplicativeRight_symm_apply_symm_apply, AddMonoidAlgebra.liftMagma_apply_apply, instProperSpaceMultiplicative, WithZero.instCanLiftMultiplicativeExpNeOfNat, LaurentSeries.valuation_LaurentSeries_equal_extension, AddMonoidAlgebra.liftNC_smul, Complex.expMonoidHom_apply, WeierstrassCurve.isMinimal_iff, RatFunc.v_def, ArchimedeanClass.FiniteResidueField.mk_ne_zero, Rat.padicValuation_eq_zero_iff, LaurentSeries.LaurentSeries_coe, AddMonoidAlgebra.liftNC_single, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff, LaurentSeries.powerSeries_ext_subring, Set.unit_valuation_eq_one, AddEquiv.toMultiplicative_symm_apply_apply, AddMonoidAlgebra.lift_unique', uliftPowersHom_apply_apply, AddChar.toMonoidHomEquiv_add, MulEquiv.multiplicativeAdditive_symm_apply, denselyOrdered_multiplicative_iff, AddMonoidAlgebra.ofMagma_apply, WithZero.le_ofAdd_iff, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, AddMonoidAlgebra.liftMagma_symm_apply, instFiniteMultiplicative, CoxeterSystem.lengthParity_simple, FunctionField.inftyValuation.X_zpow, AddAction.toPermHom_apply_symm_apply, edist_ofAdd, WithZero.lt_log_iff_exp_lt, WithZero.logEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, ArchimedeanClass.FiniteElement.val_one, IsDedekindDomain.HeightOneSpectrum.intValuation_def, FunctionField.inftyValuation.X, AddMonoidAlgebra.lift_of', MulAction.zpowersQuotientStabilizerEquiv_symm_apply, isLeftRegular_ofAdd, AddMonoidHom.toMultiplicative_apply_apply, MulEquiv.toMultiplicative_toAdditive_apply, IsDedekindDomain.HeightOneSpectrum.intValuationDef_zero, toAdd_prod, FunctionField.inftyValuedFqt.def, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, Multiplicative.isOrderedMonoid, MonoidHom.ext_mint_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, Int.toAdd_zpow, WithZeroMulInt.toNNReal_eq_one_iff, ofDual_toAdd_eq_top_iff, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq, AddEquiv.toMultiplicative_symm_apply_symm_apply, WithZero.toMulBot_coe, WithZero.exp_pos, ofAdd_sub, isCyclic_multiplicative, LaurentSeries.instLaurentSeriesComplete, IsDedekindDomain.HeightOneSpectrum.valuation_surjective, AddMonoidHom.coe_toMultiplicative_map, Submonoid.powLogEquiv_apply, AddEquiv.additiveMultiplicative_symm_apply, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero, Padic.withValUniformEquiv_cast_apply, AddSubmonoid.coe_toSubmonoid_symm_apply, LaurentSeries.valuation_coe_ratFunc, AddValuation.toValuation_apply, Padic.coe_withValRingEquiv, Padic.comap_mulValuation_eq_int_padicValuation, uniformity_multiplicative, NumberField.FinitePlace.norm_eq_one_iff_notMem, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, ofAdd_zsmul, Multiplicative.toAdd_bot, Multiplicative.toAdd_le, Int.subgroup_index_ne_zero_iff, IsCyclic.mulAutMulEquiv_symm_apply_symm_apply, WithZeroMulInt.toNNReal_strictMono, LaurentSeries.tendsto_valuation, AddSubgroup.coe_toSubgroup_apply, AddMonoidAlgebra.liftNC_one, AddEquiv.toAdditive_toMultiplicative_apply, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, AddChar.toMonoidHomEquiv_symm_mul, LaurentSeries.coe_range_dense, AddMonoidAlgebra.of_injective, PowerSeries.intValuation_X, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', MonoidHom.ext_mnat_iff, toAdd_div, WithZero.exp_zsmul, PowerSeries.coe_orderHom, Padic.coe_withValRingEquiv_symm, MulAutMultiplicative_apply_symm_apply, AddSubgroup.fg_iff_mul_fg, Real.expMonoidHom_apply, isCyclic_multiplicative_iff, Order.pred_toAdd, LocallyFiniteOrder.orderMonoidHom_strictMono, AddCommMonCat.equivalence_functor_obj_coe, LaurentSeries.comparePkg_eq_extension, NumberField.toNNReal_valued_eq_adicAbv, Multiplicative.existsMulOfLe, LaurentSeries.valuation_def, FunctionField.inftyValuation.C, AddCommMonCat.equivalence_counitIso, WithZero.log_zero, uliftZPowersHom_apply_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, IsCyclic.mulAutMulEquiv_symm_apply_apply, Submonoid.toAddSubmonoid'_closure, isOpenMap_ofAdd, AddEquiv.toMultiplicativeLeft_symm_apply_apply, Rat.HeightOneSpectrum.valuation_equiv_padicValuation, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, LaurentSeries.uniformContinuous_coeff, instDiscreteTopologyMultiplicative, AddSubsemigroup.toSubsemigroup_closure, Multiplicative.exists, ofAdd_nsmul, CoxeterSystem.lengthParity_eq_ofAdd_length, IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul', Padic.norm_rat_le_one_iff_padicValuation_le_one, AddMonoidHom.toMultiplicativeLeft_apply_apply, Set.integer_valuation_le_one, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, Rat.surjective_padicValuation, NumberField.FinitePlace.isFinitePlace, Multiplicative.forall, zpowersHom_ker_eq, not_denselyOrdered_withZero_int, CircleDeg1Lift.translationNumber_translate, Subgroup.toAddSubgroup'_closure, Multiplicative.ofAdd_mono, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Nat.toAdd_pow, AddMonCat.equivalence_functor_map, LaurentSeries.ratfuncAdicComplRingEquiv_apply, MonoidHom.coe_toAdditiveRight, IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos, AddValuation.toValuation_symm_eq, IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer, WithZero.expRecOn_zero, WithZero.toMulBot_le, FreeAbelianGroup.liftAddEquiv_apply_apply, AddSubgroup.index_toSubgroup, MonoidHom.toAdditiveLeft_symm_apply_apply, BoundedContinuousFunction.charMonoidHom_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, uniformContinuous_ofAdd, Set.integer_eq, AddValuation.ofValuation_symm_eq, isRightRegular_ofAdd, AddMonoidAlgebra.lift_def, isAddRightRegular_toAdd, MonoidHom.coe_toAdditive'', ofAdd_eq_one, Int.padicValuation_le_one, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, nnnorm_toAdd, FreeMonoid.countP_apply, LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono, Multiplicative.ext_iff, NumberField.FinitePlace.norm_le_one, IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq, Fintype.card_multiplicative, FreeMonoid.count_apply, addMonoidEndToMultiplicative_apply_apply, nhds_ofAdd, LaurentSeries.mem_integers_of_powerSeries, WithZero.log_lt_iff_lt_exp, WeierstrassCurve.IsGoodReduction.goodReduction, LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered, Multiplicative.monoidHom_ext_iff, LinearOrderedCommGroup.discrete_or_denselyOrdered, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, instContinuousMulMultiplicativeOfContinuousAdd, Multiplicative.isCancelMul, ValuationSubring.algebraMap_injective, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, LinearOrderedCommGroup.discrete_iff_not_denselyOrdered, instIsMulTorsionFreeMultiplicativeOfIsAddTorsionFree, Submonoid.powLogEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, AddMonoidHom.coe_toMultiplicative'', instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, instBoundedSpaceMultiplicative, powersMulHom_symm_apply, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq, AddMonoidAlgebra.of'_eq_of, ofAdd_toDual_eq_zero_iff, Additive.addMonoidHom_ext_iff, CircleDeg1Lift.translate_pow, Subsemigroup.toAddSubsemigroup'_closure, AddValuation.supp_quot_supp, AddValuation.ofValuation_apply, AddSubgroup.toSubgroup_comap, AddSubgroup.coe_toSubgroup_symm_apply, FunctionField.inftyValuation_apply, WithZero.le_exp_log, Multiplicative.instUniqueProdsOfUniqueSums, WithZero.val_logOrderIso_symm_apply, MonoidHom.toAdditiveRight_apply_apply, Multiplicative.smulCommClass, WithZero.toMulBot_symm_bot, instWellFoundedGTWithZeroMultiplicativeIntLeOne, instIsSuccArchimedeanMultiplicative, Multiplicative.isLeftCancelMul, ofAdd_neg, LaurentSeries.exists_ratFunc_eq_v, LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero, Monoid.fg_of_addMonoid_fg, nndist_toAdd, Padic.isDenseInducing_cast_withVal, ofAdd_image_multiples_eq_powers_ofAdd, AddSubmonoid.fg_iff_mul_fg, WithZero.exp_zero, WithZero.toMulBot_strictMono, WithZero.logEquiv_unitsMk0, WithZero.val_inv_logOrderIso_symm_apply, toAdd_list_sum, toAdd_inv, IsDedekindDomain.HeightOneSpectrum.intValuation_apply, MonoidHom.coe_toAdditive', LaurentSeries.valuation_X_pow, Multiplicative.isIsometricSMul, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem, Int.padicValuation_eq_zero_iff, Multiplicative.ofAdd_image_nsmul, NumberField.FinitePlace.norm_def, ArchimedeanClass.FiniteElement.ext_iff, uniformContinuous_toAdd, addMonoidEndToMultiplicative_symm_apply_apply, AddEquiv.toMultiplicativeLeft_apply_apply, IsDedekindDomain.selmerGroup.valuation_ker_eq, AddChar.coe_toMonoidHomEquiv_symm, LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered, Multiplicative.toAdd_top, WithZero.exp_neg, AddCommGrpCat.toCommGrp_map, Rat.padicValuation_le_one_iff, AddMonoid.fg_iff_mul_fg, LinearOrderedCommGroup.isCyclic_iff_nonempty_equiv_int, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, Multiplicative.ofAdd_top, MonoidHom.coe_toMultiplicative_ker, Polynomial.valuation_X_eq_neg_one, MulEquiv.piMultiplicative_symm_apply, WithZero.exp_injective, AddSubgroup.relIndex_toSubgroup, continuous_ofAdd, AffineEquiv.constVAddHom_apply

---

← Back to Index