Hom

📁 Source: Mathlib/Algebra/GroupWithZero/Hom.lean

Statistics

Metric	Count
Definitions MonoidWithZeroHom, coeToMonoidHom, coeToZeroHom, comp, copy, funLike, id, instInhabited, instMul, one, toMonoidHom, toZeroHom, MonoidWithZeroHomClass, toMonoidWithZeroHom, instCoeTCMonoidWithZeroHomOfMonoidWithZeroHomClass, powMonoidWithZeroHom, «term_→*₀_»	17
Theorems cancel_left, cancel_right, coe_coe, coe_comp, coe_copy, coe_mk, comp_apply, comp_assoc, comp_id, copy_eq, ext, ext_iff, id_apply, id_comp, instSubsingleton, map_ite_one_zero, map_ite_zero_one, map_mul, map_mul', map_one, map_one', map_zero, mk_coe, monoidWithZeroHomClass, one_apply_def, one_apply_eq_one_iff, one_apply_eq_zero_iff, one_apply_of_ne_zero, one_apply_zero, toMonoidHom_coe, toMonoidHom_injective, toZeroHom_coe, toZeroHom_injective, toMonoidHomClass, toZeroHomClass, of_injective, of_map, coe_powMonoidWithZeroHom, powMonoidWithZeroHom_apply	39
Total	56

MonoidWithZeroHom

Definitions

Name	Category	Theorems
coeToMonoidHom 📖	CompOp	—
coeToZeroHom 📖	CompOp	—
comp 📖	CompOp	24 math math: comp_apply, snd_comp_inl, Perfection.mk_comp_teichmuller₀, NumberField.HeightOneSpectrum.rankOne_hom'_def, GrpWithZero.hom_comp, OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, OrderMonoidWithZeroHom.toMonoidWithZeroHom_coe, one_comp, fst_comp_inl, comp_one, coe_comp, snd_comp_inr, comp_assoc, comp_id, WithZero.map'_comp, MonoidWithZeroHomClass.ext_rat_iff, Valuation.RankOne.restrict_RankOne_hom_eq, id_comp, fst_comp_inr, ext_int_iff, MonoidWithZeroHomClass.ext_nnrat_iff, cancel_right, cancel_left
copy 📖	CompOp	2 math math: coe_copy, copy_eq
funLike 📖	CompOp	650 math math: normalize_one, Quaternion.normSq_eq_zero, Valuation.mem_nhds_zero_iff, Quaternion.star_mul_self, Polynomial.degree_normalize, Quaternion.coe_normSq_add, Cardinal.toNat_ofENat, Cardinal.toNat_surjective, comp_apply, Valued.isOpen_closedball, Cardinal.toNat_ofNat, RatFunc.liftMonoidWithZeroHom_apply, GrpWithZero.forget_map, Polynomial.roots_normalize, Complex.UnitDisc.normSq_lt_one, RCLike.normSq_to_real, WithVal.valueGroupOrderIso₀_symm_apply, Ideal.finite_setOf_absNorm_le₀, Complex.normSq_pos, Valuation.isClopen_closedBall, normalize_dvd_iff, NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, WithZero.map'_mono, Ideal.absNorm_span_insert, summable_riemannZetaSummand, Complex.normSq_natCast, WithZero.map'_zero, Ideal.relNorm_smul, Valuation.isEquiv_map_self_of_strictMono, UpperHalfPlane.normSq_pos, Complex.norm_mul_self_eq_normSq, RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk, Valued.extension_extends, Cardinal.toNat_eq_iff, WithZero.map'_coe, Complex.one_le_normSq_iff, Cardinal.toNat_congr, MulChar.toMonoidWithZeroHom_apply, WithZero.lift'_symm_apply_apply, NumberField.mixedEmbedding.normAtAllPlaces_apply, signHom_apply, NumberField.mixedEmbedding.norm_eq_zero_iff', Ring.ordFrac_eq_div, gcd_mul_left, NNReal.exists_lt_of_strictMono, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isComplex, Quaternion.normSq_natCast, gcd_greatest, mrange_nontrivial, NumberField.mixedEmbedding.norm_unit_smul, Complex.nndist_self_conj, NumberField.mixedEmbedding.norm_eq_norm, NumberField.FinitePlace.norm_def', WithVal.valueGroupOrderIso₀_restrict, Ideal.finite_setOf_absNorm_eq, UpperHalfPlane.im_smul_eq_div_normSq, smulMonoidWithZeroHom_apply, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, ValueGroup₀.monoidWithZeroHom_strictMono, WithVal.valueGroupOrderIso₀_apply, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, RCLike.normSq_neg, one_apply_zero, Cardinal.toNat_mul, Valued.toUniformSpace_eq, NumberField.HeightOneSpectrum.rankOne_hom'_def, UpperHalfPlane.moebius_im, Ideal.relNorm_mono, FractionalIdeal.absNorm_eq', ModularGroup.one_lt_normSq_T_zpow_smul, Valuation.restrict_eq_one_iff, Complex.normSq_ratCast, RCLike.continuous_normSq, Ideal.relNorm_relNorm, map_eq_zero_iff, one_apply_eq_zero_iff, WithZero.map'_strictMono, Ideal.absNorm_pos_iff_mem_nonZeroDivisors, normalize_eq_normalize, Complex.normSq_mk, ValuationSubring.mapOfLE_valuation_apply, NormalizedGCDMonoid.normalize_lcm, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, GaussianInt.normSq_le_normSq_of_re_le_of_im_le, Ring.ordFrac_eq_ord, Ideal.absNorm_eq_pow_inertiaDeg', Cardinal.toNat_apply_of_aleph0_le, fst_mono, Valuation.IsEquiv.restrict, Int.normalize_of_nonneg, RatFunc.liftMonoidWithZeroHom_apply_div', Ideal.relNorm_top, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, Valued.isClopen_ball, Quaternion.normSq_smul, Ideal.relNorm_eq_pow_of_isPrime_isGalois, Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver, ValuativeRel.ValueGroupWithZero.embed_strictMono, Ideal.absNorm_mem, NumberField.mixedEmbedding.normAtPlace_apply_of_isReal, Multiset.lcm_singleton, GrpWithZero.hom_comp, Complex.normSq_mul, GrpWithZero.coe_id, Valuation.hasBasis_nhds_zero, ValuativeExtension.mapValueGroupWithZero_mk, coe_mk, ValueGroup₀.restrict₀_eq_one_iff, Quaternion.normSq_le_zero, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀, EulerProduct.eulerProduct_completely_multiplicative, Quaternion.inv_def, map_one, Valuation.restrict_le_iff, Perfection.teichmuller₀_spec, Finset.lcm_singleton, Polynomial.Monic.normalize_eq_self, gcd_eq_normalize, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, MonoidWithZero.coe_inverse, one_apply_val_unit, Valuation.restrict_eq_zero_iff, Quaternion.normSq_nonneg, Valuation.restrict_eq_mk, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, Valued.continuous_valuation, WithZeroMulInt.toNNReal_pos, GrpWithZero.coe_comp, Ideal.relNorm_singleton, Matrix.cRank_toNat_eq_rank, Ideal.map_relNorm, Valuation.restrict_lt_iff_lt_embedding, NumberField.mixedEmbedding.fundamentalCone.norm_pos_of_mem, normHom_apply, UniqueFactorizationMonoid.normalize_normalized_factor, Associates.out_mk, NumberField.HeightOneSpectrum.adicAbv_def, ValueGroup₀.embedding_unit_pos, Ideal.relNorm_le_comap, Cardinal.cast_toNat_eq_iff_lt_aleph0, normalize_eq_normalize_iff, Complex.sq_norm, ValuativeExtension.mapValueGroupWithZero_strictMono, MulEquiv.withZero_apply_symm_apply, Matrix.cRank_toNat_eq_finrank, IsValuativeTopology.isClopen_sphere, ValueGroup₀.restrict₀_of_ne_zero, inl_strictMono, Cardinal.toNat_monotoneOn, Complex.normSq_I, Polynomial.leadingCoeff_normalize, Real.nnabs_of_nonneg, WithZeroMulInt.toNNReal_lt_one_iff, RCLike.div_im, Valuation.coe_coe, Valuation.subgroups_basis, Cardinal.mk_toNat_eq_card, powMonoidWithZeroHom_apply, Valued.isOpen_sphere, Valuation.restrict_le_iff_le_embedding, Complex.tendsto_normSq_cocompact_atTop, NumberField.mixedEmbedding.convexBodySumFun_apply, WithZero.lift'_coe, NumberField.det_basisOfFractionalIdeal_eq_absNorm, RCLike.normSq_inv, FractionalIdeal.absNorm_bot, Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le, Complex.normSq_add, MulEquiv.toMonoidWithZeroHom_apply, lcm_mul_left, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, Valuation.isEquiv_restrict, Complex.re_sq_le_normSq, Complex.div_im, WithZero.map'_surjective, monoidWithZeroHomClass, NumberField.mixedEmbedding.fundamentalCone.mem_normLeOne, Valuation.RankOne.exists_val_lt, toZeroHom_coe, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, MulEquiv.withZero_apply_apply, Complex.normSq_eq_norm_sq, Valued.hasBasis_nhds_zero, Finset.gcd_mul_left, RCLike.normSq_nonneg, Finset.normalize_lcm, Ring.HasFiniteQuotients.finite_absNorm_le, Real.coe_nnabs, RatFunc.liftMonoidWithZeroHom_apply_div, NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow, OrderMonoidIso.withZero_apply_symm_apply, SignType.castHom_apply, MulEquiv.toMonoidWithZeroHom_injective, mulMonoidWithZeroHom_apply, WithZeroMulInt.toNNReal_neg_apply, RingHom.toMonoidWithZeroHom_eq_coe, Complex.normSq_sub, one_apply_def, Complex.inv_re, ValuativeExtension.mapValueGroupWithZero_valuation, Ideal.exists_relNorm_eq_pow_of_isPrime, WithZero.map'_injective, Valuation.RankOne.strictMono, ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀, Multiset.gcd_singleton, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, lipschitzWith_circleMap, range_nontrivial, EulerProduct.eulerProduct_completely_multiplicative_tprod, Associates.normalize_out, Quaternion.normSq_inv, one_apply_of_ne_zero, UniqueFactorizationMonoid.radical_of_prime, NumberField.mixedEmbedding.covolume_idealLattice, ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk, ValueGroup₀.restrict₀_range_eq_top, NumberField.mixedEmbedding.normAtPlace_add_le, Polynomial.content_C_mul, Valued.isClosed_ball, Valuation.restrict_lt_one_iff, one_apply_apply_eq, HahnSeries.map_one, map_zero, RCLike.inv_im, ValueGroup₀.embedding_apply, Valued.isClopen_sphere, Int.normalize_coe_nat, normalize_eq_zero, UpperHalfPlane.normSq_denom_pos, lcm_mul_right, Quaternion.normSq_eq_norm_mul_self, ModularGroup.normSq_S_smul_lt_one, Valued.isClosed_sphere, IsValuativeTopology.isClosed_closedBall, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, Polynomial.normalize_content, WithZeroMulInt.toNNReal_le_one_iff, Complex.inv_def, legendreSym.hom_apply, NormalizedGCDMonoid.normalize_gcd, normalize_gcd, ENat.coe_toNatHom, Complex.normSq_ofNat, Valuation.cauchy_iff, tsum_riemannZetaSummand, Ideal.relNorm_algebraMap', normalize_apply, Cardinal.toNat_rightInverse, Cardinal.toNat_strictMonoOn, Complex.normSq_ofReal_add_I_mul_sqrt_one_sub, Valuation.IsRankOneDiscrete.embedding_generator', Ideal.relNorm_int, Cardinal.toNat_le_toNat, Ideal.absNorm_dvd_absNorm_of_le, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, one_apply_eq_one_iff, NumberField.Ideal.tendsto_norm_le_div_atTop₀, inl_mul_inr_eq_mk_of_unit, OrderMonoidIso.withZero_apply_apply, NumberField.mixedEmbedding.logMap_apply_of_norm_eq_one, Cardinal.toNat_lt_iff_lt_of_lt_aleph0, ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, ValuationSubring.monotone_mapOfLE, Valuation.restrict_inj, NumberField.HeightOneSpectrum.embedding_mul_absNorm, Int.absNorm_under_mem, ValuativeRel.RankLeOneStruct.strictMono, ValueGroup₀.restrict₀_eq_zero_iff, Complex.normSq_zero, Valuation.embedding_restrict, Perfection.teichmuller₀_sModEq, Cardinal.toNat_lift, EulerProduct.eulerProduct_completely_multiplicative_hasProd, ENat.toNatHom_apply, Ideal.spanNorm_eq, FractionalIdeal.absNorm_eq, RCLike.normSq_mul, Valued.valuation_isClosedMap, summable_dirichletSummand, Cardinal.toNat_eq_one, NumberField.mixedEmbedding.norm_nonneg, Ideal.relNorm_algebraMap, Submodule.spanSingleton_apply, normalize_coe_units, Complex.normSq_conj, Complex.continuous_normSq, Perfection.teichmuller₀_spec', Quaternion.normSq_add, Valued.cauchy_iff, ModularGroup.tendsto_normSq_coprime_pair, NumberField.mixedEmbedding.norm_smul, Complex.normSq_intCast, Cardinal.toNat_toENat, Ideal.relNorm_eq_bot_iff, coe_coe, IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one, NumberField.FinitePlace.norm_def_int, inr_mono, Ideal.card_norm_le_eq_card_norm_le_add_one, NumberField.mixedEmbedding.continuous_norm, Associates.mk_normalize, Quaternion.normSq_exp, IntermediateField.relfinrank_eq_toNat_relrank, Complex.div_re, FractionalIdeal.absNorm_span_singleton, OrderMonoidWithZeroHom.coe_mk, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, toMonoidHom_coe, gcd_same, Subfield.relfinrank_eq_toNat_relrank, Valuation.restrict_pos_iff, gcd_zero_right, snd_inr, snd_inl_apply_of_ne_zero, IsValuativeTopology.isClopen_ball, Cardinal.mk_toNat_of_infinite, lcm_one_left, Valuation.restrict_def, Cardinal.toNat_eq_iff_of_lt_aleph0, inl_injective, ValueGroup₀.restrict₀_surjective, NumberField.absNorm_differentIdeal, Ideal.absNorm_top, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isReal, Ideal.absNorm_apply, Ideal.absNorm_pos_of_nonZeroDivisors, Orientation.normSq_kahler, IsLocalization.toLocalizationMap_toMonoidHom, Complex.normSq_inv, Cardinal.cast_toNat_of_aleph0_le, Valuation.isClosed_closedBall, NumberField.mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem, Int.normalize_of_nonpos, Complex.normSq_div, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, Complex.normSq_ofReal, RatFunc.liftMonoidWithZeroHom_injective, Quaternion.sq_eq_neg_normSq, Cardinal.toNat_le_iff_of_lt_aleph0, RCLike.normSq_eq_def', Real.nndist_eq, Algebra.norm_complex_apply, Complex.norm_def, IsValuativeTopology.isOpen_closedBall, Finset.gcd_singleton, apply_one_apply_eq, normalize_lcm, Cardinal.toNat_inj_of_lt_aleph0, lcm_same, Int.absNorm_under_dvd_absNorm, Valuation.toTopologicalSpace_eq, Quaternion.sq_eq_normSq, Valuation.map_apply, Cardinal.toNat_injOn, Polynomial.normalize_eq_self_iff_monic, Submodule.mker_spanSingleton, NumberField.mixedEmbedding.normAtPlace_neg, coe_powMonoidWithZeroHom, NumberField.mixedEmbedding.continuous_normAtPlace, Irreducible.normalizedFactors_pow, Int.natAbsHom_apply, GaussianInt.intCast_real_norm, Quaternion.self_mul_star, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm, Valuation.toMonoidWithZeroHom_coe_eq_coe, Cardinal.toNat_le_iff_le_of_lt_aleph0, snd_mono, UniqueFactorizationMonoid.normalizedFactors_irreducible, Int.abs_eq_normalize, Valuation.isClopen_ball, MulEquiv.toMonoidWithZeroHom_bijective, Complex.normSq_nonneg, Quaternion.normSq_def', tsum_dirichletSummand, NumberField.exists_ideal_in_class_of_norm_le, NumberField.mixedEmbedding.normAtPlace_apply, Perfection.coe_teichmuller_eq_teichmuller₀, Complex.nndist_conj_self, RCLike.normSq_pos, lcm_units_coe_left, ModularGroup.im_smul_eq_div_normSq, NumberField.Ideal.tendsto_norm_le_div_atTop, Valued.isOpen_closedBall, fst_apply_coe, fst_inl, fst_surjective, Cardinal.toNat_eq_one_iff_unique, Valuation.hasBasis_nhds, Real.nnabs_coe, withTopMap_apply, NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex, FractionalIdeal.absNorm_nonneg, gcd_zero_left, Valued.mem_nhds_zero, Valuation.RankLeOne.exists_val_lt, Valued.isOpen_ball, NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff, Ideal.natAbs_det_equiv, Complex.normSq_add_mul_I, Valued.mem_nhds, Quaternion.normSq_zpow, Ideal.absNorm_eq_one_iff, WithZeroMulInt.toNNReal_eq_one_iff, coe_comp, UniqueFactorizationMonoid.normalizedFactors_prod_eq, Quaternion.inner_self, NumberField.torsionOrder_dvd_absNorm_sub_one, Valuation.isOpen_ball, WithZero.lift'_surjective, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, count_span_normalizedFactors_eq, Real.toNNReal_abs, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, Quaternion.normSq_def, NumberField.mixedEmbedding.logMap_apply, Cardinal.toNat_lt_toNat, ValuativeRel.ValueGroupWithZero.embed_mk, inr_apply_unit, IsValuativeTopology.isClosed_ball, NumberField.mixedEmbedding.fundamentalCone.intNorm_coe, NumberField.mixedEmbedding.norm_eq_zero_iff, NumberField.mixedEmbedding.logMap_apply_of_norm_one, gcd_mul_right, val_mrange_zero, UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors, LinearOrderedCommGroupWithZero.fst_apply, WithVal.valueGroupOrderIso₀_symm_restrict, GrpWithZero.hom_id, NumberField.mixedEmbedding.normAtPlace_nonneg, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, Quaternion.normSq_neg, copy_eq, RCLike.mul_self_norm, Valuation.hasBasis_uniformity, EulerProduct.one_sub_inv_eq_geometric_of_summable_norm, dvd_normalize_iff, WithZeroMulInt.toNNReal_strictMono, Valued.toNormedField.norm_def, Valuation.toUniformSpace_eq, associated_normalize_iff, Valuation.isOpen_sphere, Multiset.normalize_lcm, Complex.mul_conj, Valuation.norm_def, Cardinal.cast_toNat_of_lt_aleph0, Cardinal.toNat_eq_zero, Complex.inv_im, RCLike.normSq_div, RCLike.im_sq_le_normSq, fst_inr_apply_of_ne_zero, NumberField.mixedEmbedding.normAtPlace_negAt, Perfection.mk_teichmuller₀, Field.finSepDegree_eq, nnnormHom_apply, Valuation.exists_div_eq_of_unit, Valuation.restrict_le_one_iff, Valuation.isClosed_ball, Circle.normSq_coe, Ideal.finite_setOf_absNorm_le, NumberField.mixedEmbedding.normAtPlace_smul, CommGroupWithZero.normalize_eq_one, Complex.one_lt_normSq_iff, ext_iff, FractionalIdeal.abs_det_basis_change, Ideal.span_singleton_absNorm, divMonoidWithZeroHom_apply, Finset.gcd_mul_right, Field.finInsepDegree_def', ValueGroup₀.embedding_restrict₀, UniqueFactorizationMonoid.mem_normalizedFactors_iff', Mathlib.Meta.Positivity.nnabs_pos_of_pos, NumberField.mixedEmbedding.norm_eq_of_normAtPlace_eq, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, RCLike.re_sq_le_normSq, inr_strictMono, mk_coe, Complex.normSq_eq_conj_mul_self, Valued.hasBasis_uniformity, FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm, WithZero.map'_surjective_iff, ValuativeRel.valuation_lt_symm_orderMonoidIso, WithZeroMulInt.toNNReal_pos_apply, Perfection.coeff_zero_symm_quotientMulEquiv, Ideal.absNorm_eq_pow_inertiaDeg, RCLike.normSq_zero, NumberField.mixedEmbedding.norm_real, ValueGroup₀.restrict₀_apply, RCLike.normSq_eq_zero, NumberField.HeightOneSpectrum.one_lt_absNorm, Valuation.restrict_lt_iff, Ideal.absNorm_eq_zero_iff, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, Cardinal.aleph0_toNat, Real.nnabs_pos, ext_nat_iff, Valued.isClosed_closedBall, Valuation.isOpen_closedBall, Cardinal.toNat_natCast, inl_mono, UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow, Quaternion.normSq_intCast, Polynomial.content_C, Valuation.RankOne.isNontrivial_restrict, ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq, Ideal.absNorm_bot, Ideal.relNorm_apply, UniqueFactorizationMonoid.prod_normalizedFactors_eq, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, Complex.normSq_apply, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, RCLike.normSq_to_complex, map_mul, ValuativeRel.restrict_lt_orderMonoidIso, RCLike.normSq_add, UniqueFactorizationMonoid.radical_pow_of_prime, RCLike.div_re, Cardinal.toNat_apply_of_lt_aleph0, Complex.im_sq_le_normSq, Int.ideal_span_absNorm_eq_self, Ideal.relNorm_bot, Ideal.norm_mem_relNorm, Valuation.coe_mk, Cardinal.toNat_lift_add_lift, Submonoid.LocalizationMap.lift₀_apply, normalize_eq_one, id_apply, Cardinal.toNat_pos, WithZero.lift'_zero, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, RCLike.sqrt_normSq_eq_norm, NumberField.FinitePlace.norm_embedding', snd_apply_coe, MonoidWithZero.inverse_apply, Cardinal.toNat_add, Ideal.absNorm_relNorm, Valuation.restrict_exists_div_eq, RCLike.normSq_apply, Int.absNorm_under_eq_sInf, Ideal.absNorm_span_singleton, Valuation.IsEquiv.orderMonoidIso_spec, FractionalIdeal.coeIdeal_absNorm, Valuation.RankOne.hom_eq_zero_iff, lcm_units_coe_right, Quaternion.im_sq, Ideal.absNorm_algebraMap, Multiset.normalize_gcd, Valued.isClopen_closedBall, Valuation.RankOne.restrict_RankOne_hom_eq, AbsoluteValue.coe_toMonoidWithZeroHom, LinearOrderedCommGroupWithZero.inl_apply, Int.cast_mem_ideal_iff, LinearOrderedCommGroupWithZero.inr_apply, Ideal.relNorm_map_algEquiv, normalize_associated, OrderMonoidWithZeroHom.coe_monoidWithZeroHom, FractionalIdeal.absNorm_eq_zero_iff, ValueGroup₀.instIsOrderedMonoid, RCLike.normSq_one, Ideal.span_singleton_absNorm_le, Polynomial.monic_normalize, Real.nndist_eq', Ideal.natAbs_det_basis_change, Perfection.teichmuller₀_mapMonoidHom_idealQuotientMk, Valuation.RankLeOne.strictMono', Multiset.gcd_map_mul, NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, Quaternion.normSq_div, Valuation.exists_setOf_restrict_le_iff, inr_injective, Ideal.ringChar_quot, Complex.normSq_neg, Real.exists_lt_of_strictMono, WithZero.map'_id, commute_inl_inr, NumberField.mixedEmbedding.norm_negAt, normalize_zero, NumberField.mixedEmbedding.norm_unit, Int.liesOver_span_absNorm, UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors, IsValuativeTopology.isOpen_sphere, Quaternion.normSq_star, UpperHalfPlane.c_mul_im_sq_le_normSq_denom, Cardinal.zero_toNat, ValuationSubring.mapOfLE_comp_valuation, ext_int_iff, normalize_idem, Complex.range_normSq, Quaternion.normSq_ratCast, NumberField.FinitePlace.norm_embedding_int, UpperHalfPlane.smulAux'_im, Finset.normalize_gcd, lcm_eq_normalize, Quaternion.continuous_normSq, ValueGroup₀.embedding_strictMono, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, Complex.normSq_ofReal_sub_I_mul_sqrt_one_sub, Cardinal.aleph_toNat, Ideal.relNorm_eq_pow_of_isMaximal, Cardinal.natCast_toNat_le, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, Complex.normSq_eq_zero, RCLike.normSq_sub, Submonoid.LocalizationMap.lift₀_def, Nat.absNorm_under_prime, IsValuativeTopology.isClopen_closedBall, Valuation.mem_nhds_iff, GaussianInt.normSq_div_sub_div_lt_one, Int.nonneg_iff_normalize_eq_self, ENatMap_apply, normalize_eq_normalize_iff_associated, GaussianInt.intCast_complex_norm, NumberField.FinitePlace.norm_def, EulerProduct.exp_tsum_primes_log_eq_tsum, PowerSeries.X_eq_normalizeX, Quaternion.normSq_coe, inl_apply_unit, Ideal.relNorm_comap_algEquiv, Valuation.is_topological_valuation, Cardinal.toNat_eq_ofNat, Real.cast_natAbs_eq_nnabs_cast, Cardinal.one_toNat, normalize_associated_iff, Polynomial.X_eq_normalize, snd_surjective, Valuation.isClopen_sphere, Cardinal.continuum_toNat, Polynomial.content_monomial, Polynomial.map_normalize, normalize_eq, NumberField.mixedEmbedding.norm_apply, Valuation.isClosed_sphere, RCLike.normSq_conj, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, RCLike.inv_re, Complex.normSq_one, NumberField.mixedEmbedding.normAtPlace_real, MulEquiv.toMonoidWithZeroHom_surjective, lcm_one_right, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, Valued.extensionValuation_toFun, WithZero.map'_injective_iff, Ideal.absNorm_dvd_norm_of_mem, Perfection.teichmullerFun_eq_teichmuller₀, associated_normalize, WithZero.map'_map', FractionalIdeal.absNorm_one
id 📖	CompOp	6 math math: fst_comp_inl, snd_comp_inr, GrpWithZero.hom_id, comp_id, id_apply, id_comp
instInhabited 📖	CompOp	—
instMul 📖	CompOp	—
one 📖	CompOp	13 math math: snd_comp_inl, one_apply_zero, one_apply_eq_zero_iff, one_apply_val_unit, Valuation.toMonoidWithZeroHom_one, one_apply_def, one_comp, one_apply_of_ne_zero, one_apply_apply_eq, comp_one, one_apply_eq_one_iff, apply_one_apply_eq, fst_comp_inr
toMonoidHom 📖	CompOp	15 math math: Submodule.ker_unitsToPic, WithZero.monoidWithZeroHom_ext_iff, Algebra.norm_complex_eq, WithZero.lift'_unique, toMonoidHom_coe, Submodule.unitsQuotEquivRelPic_symm_apply, Matrix.ProjGenLinGroup.signDet_mk, ClassGroup.equivPic_symm_apply, Perfection.teichmuller_eq_teichmuller₀_toMonoidHom, Submodule.mulExact_unitsMap_spanSingleton_unitsToPic, toMonoidHom_injective, Submonoid.LocalizationMap.lift₀_apply, ClassGroup.equivPic_apply, Submodule.ker_unitsMap_spanSingleton, Submodule.unitsQuotEquivRelPic_apply_coe
toZeroHom 📖	CompOp	10 math math: OrderMonoidWithZeroHom.toFun_eq_coe, Valuation.toFun_eq_coe, OrderMonoidWithZeroHom.monotone', toZeroHom_coe, RingHom.ENatMap_apply, Valuation.map_add_le_max', map_one', RingHom.withTopMap_apply, map_mul', toZeroHom_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cancel_left 📖	mathematical	DFunLike.coe MonoidWithZeroHom funLike	comp	—	ext comp_apply
cancel_right 📖	mathematical	DFunLike.coe MonoidWithZeroHom funLike	comp	—	ext Function.Surjective.forall DFunLike.ext_iff
coe_coe 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike MonoidWithZeroHomClass.toMonoidWithZeroHom	—	—
coe_comp 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe MonoidWithZeroHom funLike	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidHom.instFunLike copy	—	—
coe_mk 📖	mathematical	ZeroHom.toFun MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MulOne.toMul	DFunLike.coe MonoidWithZeroHom funLike ZeroHom MulZeroClass.toZero MulZeroOneClass.toMulZeroClass ZeroHom.funLike	—	—
comp_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
copy_eq 📖	mathematical	DFunLike.coe MonoidWithZeroHom funLike	copy MonoidHomClass.toMonoidHom MonoidWithZeroHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass funLike MonoidWithZeroHomClass.toMonoidHomClass monoidWithZeroHomClass	—	DFunLike.ext' MonoidWithZeroHomClass.toMonoidHomClass monoidWithZeroHomClass
ext 📖	—	DFunLike.coe MonoidWithZeroHom funLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike id	—	—
id_comp 📖	mathematical	—	comp id	—	ext
instSubsingleton 📖	mathematical	—	MonoidWithZeroHom	—	Subsingleton.of_oneHomClass MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass monoidWithZeroHomClass
map_ite_one_zero 📖	mathematical	—	DFunLike.coe MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass
map_ite_zero_one 📖	mathematical	—	DFunLike.coe MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	map_zero MonoidWithZeroHomClass.toZeroHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
map_mul 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike MulZeroClass.toMul MulZeroOneClass.toMulZeroClass	—	map_mul'
map_mul' 📖	mathematical	—	ZeroHom.toFun MulZeroClass.toZero MulZeroOneClass.toMulZeroClass toZeroHom MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	—
map_one 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	map_one'
map_one' 📖	mathematical	—	ZeroHom.toFun MulZeroClass.toZero MulZeroOneClass.toMulZeroClass toZeroHom MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	—
map_zero 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	ZeroHom.map_zero'
mk_coe 📖	mathematical	ZeroHom.toFun MulZeroClass.toZero MulZeroOneClass.toMulZeroClass ZeroHomClass.toZeroHom MonoidWithZeroHom funLike MonoidWithZeroHomClass.toZeroHomClass monoidWithZeroHomClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MulOne.toMul	ZeroHomClass.toZeroHom MonoidWithZeroHom MulZeroClass.toZero MulZeroOneClass.toMulZeroClass funLike MonoidWithZeroHomClass.toZeroHomClass monoidWithZeroHomClass	—	MonoidWithZeroHomClass.toZeroHomClass monoidWithZeroHomClass ext
monoidWithZeroHomClass 📖	mathematical	—	MonoidWithZeroHomClass MonoidWithZeroHom funLike	—	map_mul' map_one' ZeroHom.map_zero'
one_apply_def 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike one MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	—
one_apply_eq_one_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike one MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	eq_or_ne one_apply_zero NeZero.one one_apply_of_ne_zero
one_apply_eq_zero_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike one MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	eq_or_ne one_apply_zero one_apply_of_ne_zero NeZero.one
one_apply_of_ne_zero 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike one MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	—
one_apply_zero 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike one MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	—
toMonoidHom_coe 📖	mathematical	—	OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidHom.toOneHom toMonoidHom DFunLike.coe MonoidWithZeroHom funLike	—	—
toMonoidHom_injective 📖	mathematical	—	MonoidWithZeroHom MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass toMonoidHom	—	Function.Injective.of_comp DFunLike.coe_injective
toZeroHom_coe 📖	mathematical	—	DFunLike.coe ZeroHom MulZeroClass.toZero MulZeroOneClass.toMulZeroClass ZeroHom.funLike toZeroHom MonoidWithZeroHom funLike	—	—
toZeroHom_injective 📖	mathematical	—	MonoidWithZeroHom ZeroHom MulZeroClass.toZero MulZeroOneClass.toMulZeroClass toZeroHom	—	Function.Injective.of_comp DFunLike.coe_injective

MonoidWithZeroHomClass

Definitions

Name	Category	Theorems
toMonoidWithZeroHom 📖	CompOp	89 math math: Valuation.mem_nhds_zero_iff, Valued.isOpen_closedball, Valuation.isClopen_closedBall, Perfection.mk_comp_teichmuller₀, Valued.extension_extends, WithVal.valueGroupOrderIso₀_restrict, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, Valuation.restrict_eq_one_iff, Valuation.IsEquiv.restrict, Valued.isClopen_ball, Valuation.hasBasis_nhds_zero, OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe, Valuation.restrict_le_iff, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, Valuation.restrict_eq_zero_iff, Valuation.restrict_eq_mk, Valued.continuous_valuation, Valuation.restrict_lt_iff_lt_embedding, IsValuativeTopology.isClopen_sphere, Valuation.coe_coe, Valued.isOpen_sphere, Valuation.restrict_le_iff_le_embedding, OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom, Valuation.isEquiv_restrict, OrderMonoidWithZeroHom.toMonoidWithZeroHom_coe, Valuation.RankOne.exists_val_lt, Valued.hasBasis_nhds_zero, GrpWithZero.Iso.mk_hom, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, Valued.isClosed_ball, Valuation.restrict_lt_one_iff, Valued.isClopen_sphere, Valued.isClosed_sphere, IsValuativeTopology.isClosed_closedBall, Valuation.cauchy_iff, Valuation.restrict_inj, Valuation.embedding_restrict, Valued.valuation_isClosedMap, Valued.cauchy_iff, MonoidWithZeroHom.coe_coe, OrderMonoidWithZeroHom.toMonoidWithZeroHom_mk, Valuation.restrict_pos_iff, IsValuativeTopology.isClopen_ball, WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv, Valuation.restrict_def, IsLocalization.toLocalizationMap_toMonoidHom, Valuation.isClosed_closedBall, IsValuativeTopology.isOpen_closedBall, OrderMonoidWithZeroHom.mk_coe, Valuation.isClopen_ball, Valued.isOpen_closedBall, Valuation.hasBasis_nhds, Valued.mem_nhds_zero, Valuation.RankLeOne.exists_val_lt, Valued.isOpen_ball, Valued.mem_nhds, Valuation.isOpen_ball, IsValuativeTopology.isClosed_ball, WithVal.valueGroupOrderIso₀_symm_restrict, Valuation.hasBasis_uniformity, Valued.toNormedField.norm_def, Valuation.isOpen_sphere, Valuation.norm_def, Valuation.exists_div_eq_of_unit, Valuation.restrict_le_one_iff, Valuation.isClosed_ball, Valued.hasBasis_uniformity, ValuativeRel.valuation_lt_symm_orderMonoidIso, Valuation.restrict_lt_iff, Valued.isClosed_closedBall, Valuation.isOpen_closedBall, Valuation.RankOne.isNontrivial_restrict, ValuativeRel.restrict_lt_orderMonoidIso, ext_rat_iff, Valuation.restrict_exists_div_eq, Valuation.IsEquiv.orderMonoidIso_spec, Valued.isClopen_closedBall, Valuation.RankOne.restrict_RankOne_hom_eq, OrderMonoidWithZeroHom.coe_monoidWithZeroHom, Valuation.exists_setOf_restrict_le_iff, IsValuativeTopology.isOpen_sphere, ext_nnrat_iff, IsValuativeTopology.isClopen_closedBall, Valuation.mem_nhds_iff, Valuation.is_topological_valuation, Valuation.isClopen_sphere, Valuation.isClosed_sphere, GrpWithZero.Iso.mk_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMonoidHomClass 📖	mathematical	—	MonoidHomClass MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	—
toZeroHomClass 📖	mathematical	—	ZeroHomClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	—

NeZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_injective 📖	mathematical	DFunLike.coe	DFunLike.coe	—	ZeroHomClass.map_zero
of_map 📖	—	—	—	—	ZeroHomClass.map_zero

(root)

Definitions

Name	Category	Theorems
MonoidWithZeroHom 📖	CompData	661 math math: normalize_one, Quaternion.normSq_eq_zero, Valuation.mem_nhds_zero_iff, Quaternion.star_mul_self, Polynomial.degree_normalize, Quaternion.coe_normSq_add, Cardinal.toNat_ofENat, Cardinal.toNat_surjective, MonoidWithZeroHom.comp_apply, Valued.isOpen_closedball, Cardinal.toNat_ofNat, RatFunc.liftMonoidWithZeroHom_apply, GrpWithZero.forget_map, Polynomial.roots_normalize, Complex.UnitDisc.normSq_lt_one, RCLike.normSq_to_real, WithVal.valueGroupOrderIso₀_symm_apply, Ideal.finite_setOf_absNorm_le₀, Complex.normSq_pos, Valuation.isClopen_closedBall, normalize_dvd_iff, NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, WithZero.map'_mono, Ideal.absNorm_span_insert, summable_riemannZetaSummand, Complex.normSq_natCast, WithZero.map'_zero, Ideal.relNorm_smul, MonoidWithZeroHom.snd_comp_inl, Valuation.isEquiv_map_self_of_strictMono, UpperHalfPlane.normSq_pos, Complex.norm_mul_self_eq_normSq, RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk, Valued.extension_extends, Cardinal.toNat_eq_iff, WithZero.map'_coe, Complex.one_le_normSq_iff, Cardinal.toNat_congr, MulChar.toMonoidWithZeroHom_apply, WithZero.lift'_symm_apply_apply, NumberField.mixedEmbedding.normAtAllPlaces_apply, signHom_apply, NumberField.mixedEmbedding.norm_eq_zero_iff', Ring.ordFrac_eq_div, gcd_mul_left, NNReal.exists_lt_of_strictMono, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isComplex, Quaternion.normSq_natCast, gcd_greatest, MonoidWithZeroHom.mrange_nontrivial, NumberField.mixedEmbedding.norm_unit_smul, Complex.nndist_self_conj, NumberField.mixedEmbedding.norm_eq_norm, NumberField.FinitePlace.norm_def', WithVal.valueGroupOrderIso₀_restrict, Ideal.finite_setOf_absNorm_eq, UpperHalfPlane.im_smul_eq_div_normSq, smulMonoidWithZeroHom_apply, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, MonoidWithZeroHom.ValueGroup₀.monoidWithZeroHom_strictMono, WithVal.valueGroupOrderIso₀_apply, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, RCLike.normSq_neg, MonoidWithZeroHom.one_apply_zero, Cardinal.toNat_mul, Valued.toUniformSpace_eq, NumberField.HeightOneSpectrum.rankOne_hom'_def, UpperHalfPlane.moebius_im, Ideal.relNorm_mono, FractionalIdeal.absNorm_eq', ModularGroup.one_lt_normSq_T_zpow_smul, Valuation.restrict_eq_one_iff, Complex.normSq_ratCast, RCLike.continuous_normSq, Ideal.relNorm_relNorm, MonoidWithZeroHom.map_eq_zero_iff, MonoidWithZeroHom.one_apply_eq_zero_iff, WithZero.map'_strictMono, Ideal.absNorm_pos_iff_mem_nonZeroDivisors, normalize_eq_normalize, Complex.normSq_mk, ValuationSubring.mapOfLE_valuation_apply, NormalizedGCDMonoid.normalize_lcm, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, GaussianInt.normSq_le_normSq_of_re_le_of_im_le, Ring.ordFrac_eq_ord, Ideal.absNorm_eq_pow_inertiaDeg', Cardinal.toNat_apply_of_aleph0_le, MonoidWithZeroHom.fst_mono, Valuation.IsEquiv.restrict, Int.normalize_of_nonneg, RatFunc.liftMonoidWithZeroHom_apply_div', Ideal.relNorm_top, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, Valued.isClopen_ball, Quaternion.normSq_smul, Ideal.relNorm_eq_pow_of_isPrime_isGalois, Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver, ValuativeRel.ValueGroupWithZero.embed_strictMono, Ideal.absNorm_mem, NumberField.mixedEmbedding.normAtPlace_apply_of_isReal, Multiset.lcm_singleton, GrpWithZero.hom_comp, Complex.normSq_mul, GrpWithZero.coe_id, Valuation.hasBasis_nhds_zero, ValuativeExtension.mapValueGroupWithZero_mk, MonoidWithZeroHom.coe_mk, MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_one_iff, Quaternion.normSq_le_zero, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀, EulerProduct.eulerProduct_completely_multiplicative, Quaternion.inv_def, MonoidWithZeroHom.map_one, Valuation.restrict_le_iff, Perfection.teichmuller₀_spec, Finset.lcm_singleton, Polynomial.Monic.normalize_eq_self, gcd_eq_normalize, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, MonoidWithZero.coe_inverse, MonoidWithZeroHom.one_apply_val_unit, Valuation.restrict_eq_zero_iff, Quaternion.normSq_nonneg, Valuation.restrict_eq_mk, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, Valued.continuous_valuation, WithZeroMulInt.toNNReal_pos, GrpWithZero.coe_comp, Ideal.relNorm_singleton, Matrix.cRank_toNat_eq_rank, Ideal.map_relNorm, Valuation.restrict_lt_iff_lt_embedding, NumberField.mixedEmbedding.fundamentalCone.norm_pos_of_mem, normHom_apply, UniqueFactorizationMonoid.normalize_normalized_factor, Associates.out_mk, NumberField.HeightOneSpectrum.adicAbv_def, MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos, Ideal.relNorm_le_comap, Cardinal.cast_toNat_eq_iff_lt_aleph0, normalize_eq_normalize_iff, Complex.sq_norm, ValuativeExtension.mapValueGroupWithZero_strictMono, MulEquiv.withZero_apply_symm_apply, Matrix.cRank_toNat_eq_finrank, IsValuativeTopology.isClopen_sphere, MonoidWithZeroHom.ValueGroup₀.restrict₀_of_ne_zero, MonoidWithZeroHom.inl_strictMono, Cardinal.toNat_monotoneOn, Complex.normSq_I, Polynomial.leadingCoeff_normalize, Real.nnabs_of_nonneg, WithZeroMulInt.toNNReal_lt_one_iff, RCLike.div_im, Valuation.coe_coe, Valuation.subgroups_basis, Cardinal.mk_toNat_eq_card, powMonoidWithZeroHom_apply, Valued.isOpen_sphere, Valuation.restrict_le_iff_le_embedding, Complex.tendsto_normSq_cocompact_atTop, NumberField.mixedEmbedding.convexBodySumFun_apply, WithZero.lift'_coe, NumberField.det_basisOfFractionalIdeal_eq_absNorm, RCLike.normSq_inv, FractionalIdeal.absNorm_bot, Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le, Complex.normSq_add, MulEquiv.toMonoidWithZeroHom_apply, lcm_mul_left, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, Valuation.isEquiv_restrict, Complex.re_sq_le_normSq, Complex.div_im, WithZero.map'_surjective, MonoidWithZeroHom.monoidWithZeroHomClass, NumberField.mixedEmbedding.fundamentalCone.mem_normLeOne, Valuation.RankOne.exists_val_lt, MonoidWithZeroHom.toZeroHom_coe, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, MulEquiv.withZero_apply_apply, Complex.normSq_eq_norm_sq, Valued.hasBasis_nhds_zero, Finset.gcd_mul_left, RCLike.normSq_nonneg, Finset.normalize_lcm, Ring.HasFiniteQuotients.finite_absNorm_le, Real.coe_nnabs, RatFunc.liftMonoidWithZeroHom_apply_div, Valuation.toMonoidWithZeroHom_one, NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow, OrderMonoidIso.withZero_apply_symm_apply, SignType.castHom_apply, MulEquiv.toMonoidWithZeroHom_injective, mulMonoidWithZeroHom_apply, WithZeroMulInt.toNNReal_neg_apply, RingHom.toMonoidWithZeroHom_eq_coe, Complex.normSq_sub, MonoidWithZeroHom.one_apply_def, Complex.inv_re, ValuativeExtension.mapValueGroupWithZero_valuation, Ideal.exists_relNorm_eq_pow_of_isPrime, WithZero.map'_injective, Valuation.RankOne.strictMono, ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀, MonoidWithZeroHom.one_comp, Multiset.gcd_singleton, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, lipschitzWith_circleMap, MonoidWithZeroHom.range_nontrivial, EulerProduct.eulerProduct_completely_multiplicative_tprod, Associates.normalize_out, Quaternion.normSq_inv, MonoidWithZeroHom.one_apply_of_ne_zero, UniqueFactorizationMonoid.radical_of_prime, NumberField.mixedEmbedding.covolume_idealLattice, ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk, MonoidWithZeroHom.ValueGroup₀.restrict₀_range_eq_top, NumberField.mixedEmbedding.normAtPlace_add_le, Polynomial.content_C_mul, Valued.isClosed_ball, Valuation.restrict_lt_one_iff, MonoidWithZeroHom.one_apply_apply_eq, HahnSeries.map_one, MonoidWithZeroHom.map_zero, RCLike.inv_im, MonoidWithZeroHom.ValueGroup₀.embedding_apply, Valued.isClopen_sphere, Int.normalize_coe_nat, normalize_eq_zero, UpperHalfPlane.normSq_denom_pos, lcm_mul_right, Quaternion.normSq_eq_norm_mul_self, ModularGroup.normSq_S_smul_lt_one, Valued.isClosed_sphere, IsValuativeTopology.isClosed_closedBall, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, Polynomial.normalize_content, WithZeroMulInt.toNNReal_le_one_iff, Complex.inv_def, legendreSym.hom_apply, NormalizedGCDMonoid.normalize_gcd, normalize_gcd, ENat.coe_toNatHom, Complex.normSq_ofNat, Valuation.cauchy_iff, tsum_riemannZetaSummand, Ideal.relNorm_algebraMap', normalize_apply, Cardinal.toNat_rightInverse, Cardinal.toNat_strictMonoOn, Complex.normSq_ofReal_add_I_mul_sqrt_one_sub, Valuation.IsRankOneDiscrete.embedding_generator', Ideal.relNorm_int, Cardinal.toNat_le_toNat, Ideal.absNorm_dvd_absNorm_of_le, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, MonoidWithZeroHom.comp_one, MonoidWithZeroHom.one_apply_eq_one_iff, NumberField.Ideal.tendsto_norm_le_div_atTop₀, MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit, OrderMonoidIso.withZero_apply_apply, NumberField.mixedEmbedding.logMap_apply_of_norm_eq_one, Cardinal.toNat_lt_iff_lt_of_lt_aleph0, ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, ValuationSubring.monotone_mapOfLE, Valuation.restrict_inj, NumberField.HeightOneSpectrum.embedding_mul_absNorm, Int.absNorm_under_mem, ValuativeRel.RankLeOneStruct.strictMono, MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff, WithZero.lift'_unique, Complex.normSq_zero, Valuation.embedding_restrict, Perfection.teichmuller₀_sModEq, Cardinal.toNat_lift, EulerProduct.eulerProduct_completely_multiplicative_hasProd, ENat.toNatHom_apply, Ideal.spanNorm_eq, FractionalIdeal.absNorm_eq, RCLike.normSq_mul, Valued.valuation_isClosedMap, summable_dirichletSummand, Cardinal.toNat_eq_one, NumberField.mixedEmbedding.norm_nonneg, Ideal.relNorm_algebraMap, Submodule.spanSingleton_apply, normalize_coe_units, Complex.normSq_conj, Complex.continuous_normSq, Perfection.teichmuller₀_spec', Quaternion.normSq_add, Valued.cauchy_iff, ModularGroup.tendsto_normSq_coprime_pair, NumberField.mixedEmbedding.norm_smul, Complex.normSq_intCast, Cardinal.toNat_toENat, Ideal.relNorm_eq_bot_iff, MonoidWithZeroHom.coe_coe, IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one, NumberField.FinitePlace.norm_def_int, MonoidWithZeroHom.inr_mono, Ideal.card_norm_le_eq_card_norm_le_add_one, NumberField.mixedEmbedding.continuous_norm, Associates.mk_normalize, Quaternion.normSq_exp, IntermediateField.relfinrank_eq_toNat_relrank, Complex.div_re, FractionalIdeal.absNorm_span_singleton, OrderMonoidWithZeroHom.coe_mk, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, MonoidWithZeroHom.toMonoidHom_coe, gcd_same, Subfield.relfinrank_eq_toNat_relrank, Valuation.restrict_pos_iff, gcd_zero_right, MonoidWithZeroHom.snd_inr, MonoidWithZeroHom.snd_inl_apply_of_ne_zero, IsValuativeTopology.isClopen_ball, WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv, Cardinal.mk_toNat_of_infinite, lcm_one_left, Valuation.restrict_def, Cardinal.toNat_eq_iff_of_lt_aleph0, MonoidWithZeroHom.inl_injective, MonoidWithZeroHom.instSubsingleton, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective, NumberField.absNorm_differentIdeal, Ideal.absNorm_top, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isReal, Ideal.absNorm_apply, Ideal.absNorm_pos_of_nonZeroDivisors, Orientation.normSq_kahler, IsLocalization.toLocalizationMap_toMonoidHom, Complex.normSq_inv, Cardinal.cast_toNat_of_aleph0_le, Valuation.isClosed_closedBall, NumberField.mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem, Int.normalize_of_nonpos, Complex.normSq_div, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, Complex.normSq_ofReal, RatFunc.liftMonoidWithZeroHom_injective, Quaternion.sq_eq_neg_normSq, Cardinal.toNat_le_iff_of_lt_aleph0, RCLike.normSq_eq_def', Real.nndist_eq, Algebra.norm_complex_apply, Complex.norm_def, IsValuativeTopology.isOpen_closedBall, Finset.gcd_singleton, MonoidWithZeroHom.apply_one_apply_eq, normalize_lcm, Cardinal.toNat_inj_of_lt_aleph0, lcm_same, Int.absNorm_under_dvd_absNorm, Valuation.toTopologicalSpace_eq, Quaternion.sq_eq_normSq, Valuation.map_apply, Cardinal.toNat_injOn, Polynomial.normalize_eq_self_iff_monic, Submodule.mker_spanSingleton, NumberField.mixedEmbedding.normAtPlace_neg, coe_powMonoidWithZeroHom, NumberField.mixedEmbedding.continuous_normAtPlace, Irreducible.normalizedFactors_pow, Int.natAbsHom_apply, GaussianInt.intCast_real_norm, Quaternion.self_mul_star, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm, Valuation.toMonoidWithZeroHom_coe_eq_coe, Cardinal.toNat_le_iff_le_of_lt_aleph0, MonoidWithZeroHom.snd_mono, UniqueFactorizationMonoid.normalizedFactors_irreducible, Int.abs_eq_normalize, Valuation.isClopen_ball, MulEquiv.toMonoidWithZeroHom_bijective, Complex.normSq_nonneg, Quaternion.normSq_def', tsum_dirichletSummand, NumberField.exists_ideal_in_class_of_norm_le, NumberField.mixedEmbedding.normAtPlace_apply, Perfection.coe_teichmuller_eq_teichmuller₀, Complex.nndist_conj_self, RCLike.normSq_pos, lcm_units_coe_left, ModularGroup.im_smul_eq_div_normSq, NumberField.Ideal.tendsto_norm_le_div_atTop, Valued.isOpen_closedBall, MonoidWithZeroHom.fst_apply_coe, MonoidWithZeroHom.fst_inl, MonoidWithZeroHom.fst_surjective, Cardinal.toNat_eq_one_iff_unique, Valuation.hasBasis_nhds, Real.nnabs_coe, MonoidWithZeroHom.withTopMap_apply, NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex, FractionalIdeal.absNorm_nonneg, gcd_zero_left, Valued.mem_nhds_zero, Valuation.RankLeOne.exists_val_lt, Valued.isOpen_ball, NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff, Ideal.natAbs_det_equiv, Complex.normSq_add_mul_I, Valued.mem_nhds, Quaternion.normSq_zpow, Ideal.absNorm_eq_one_iff, WithZeroMulInt.toNNReal_eq_one_iff, MonoidWithZeroHom.coe_comp, UniqueFactorizationMonoid.normalizedFactors_prod_eq, Quaternion.inner_self, NumberField.torsionOrder_dvd_absNorm_sub_one, Valuation.isOpen_ball, WithZero.lift'_surjective, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, count_span_normalizedFactors_eq, Real.toNNReal_abs, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, Quaternion.normSq_def, NumberField.mixedEmbedding.logMap_apply, Cardinal.toNat_lt_toNat, ValuativeRel.ValueGroupWithZero.embed_mk, MonoidWithZeroHom.inr_apply_unit, IsValuativeTopology.isClosed_ball, NumberField.mixedEmbedding.fundamentalCone.intNorm_coe, NumberField.mixedEmbedding.norm_eq_zero_iff, NumberField.mixedEmbedding.logMap_apply_of_norm_one, gcd_mul_right, MonoidWithZeroHom.val_mrange_zero, UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors, LinearOrderedCommGroupWithZero.fst_apply, WithVal.valueGroupOrderIso₀_symm_restrict, GrpWithZero.hom_id, NumberField.mixedEmbedding.normAtPlace_nonneg, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, Quaternion.normSq_neg, MonoidWithZeroHom.copy_eq, RCLike.mul_self_norm, Valuation.hasBasis_uniformity, EulerProduct.one_sub_inv_eq_geometric_of_summable_norm, dvd_normalize_iff, WithZeroMulInt.toNNReal_strictMono, Valued.toNormedField.norm_def, Valuation.toUniformSpace_eq, associated_normalize_iff, Valuation.isOpen_sphere, Multiset.normalize_lcm, Complex.mul_conj, Valuation.norm_def, Cardinal.cast_toNat_of_lt_aleph0, Cardinal.toNat_eq_zero, Complex.inv_im, RCLike.normSq_div, RCLike.im_sq_le_normSq, MonoidWithZeroHom.fst_inr_apply_of_ne_zero, NumberField.mixedEmbedding.normAtPlace_negAt, Perfection.mk_teichmuller₀, Field.finSepDegree_eq, nnnormHom_apply, Valuation.exists_div_eq_of_unit, Valuation.restrict_le_one_iff, Valuation.isClosed_ball, Circle.normSq_coe, Ideal.finite_setOf_absNorm_le, NumberField.mixedEmbedding.normAtPlace_smul, CommGroupWithZero.normalize_eq_one, Complex.one_lt_normSq_iff, MonoidWithZeroHom.ext_iff, FractionalIdeal.abs_det_basis_change, Ideal.span_singleton_absNorm, divMonoidWithZeroHom_apply, Finset.gcd_mul_right, Field.finInsepDegree_def', MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀, UniqueFactorizationMonoid.mem_normalizedFactors_iff', Mathlib.Meta.Positivity.nnabs_pos_of_pos, NumberField.mixedEmbedding.norm_eq_of_normAtPlace_eq, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, RCLike.re_sq_le_normSq, MonoidWithZeroHom.inr_strictMono, MonoidWithZeroHom.mk_coe, Complex.normSq_eq_conj_mul_self, Valued.hasBasis_uniformity, FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm, WithZero.map'_surjective_iff, ValuativeRel.valuation_lt_symm_orderMonoidIso, WithZeroMulInt.toNNReal_pos_apply, Perfection.coeff_zero_symm_quotientMulEquiv, Ideal.absNorm_eq_pow_inertiaDeg, RCLike.normSq_zero, OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective, NumberField.mixedEmbedding.norm_real, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply, RCLike.normSq_eq_zero, NumberField.HeightOneSpectrum.one_lt_absNorm, Valuation.restrict_lt_iff, Ideal.absNorm_eq_zero_iff, MonoidWithZeroHom.toMonoidHom_injective, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, Cardinal.aleph0_toNat, Real.nnabs_pos, MonoidWithZeroHom.ext_nat_iff, Valued.isClosed_closedBall, Valuation.isOpen_closedBall, Cardinal.toNat_natCast, MonoidWithZeroHom.inl_mono, UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow, Quaternion.normSq_intCast, Polynomial.content_C, Valuation.RankOne.isNontrivial_restrict, ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq, Ideal.absNorm_bot, Ideal.relNorm_apply, UniqueFactorizationMonoid.prod_normalizedFactors_eq, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, Complex.normSq_apply, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, RCLike.normSq_to_complex, MonoidWithZeroHom.map_mul, ValuativeRel.restrict_lt_orderMonoidIso, RCLike.normSq_add, UniqueFactorizationMonoid.radical_pow_of_prime, RCLike.div_re, Cardinal.toNat_apply_of_lt_aleph0, Complex.im_sq_le_normSq, Int.ideal_span_absNorm_eq_self, Ideal.relNorm_bot, Ideal.norm_mem_relNorm, Valuation.coe_mk, Cardinal.toNat_lift_add_lift, Submonoid.LocalizationMap.lift₀_apply, normalize_eq_one, MonoidWithZeroHom.id_apply, Cardinal.toNat_pos, WithZero.lift'_zero, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, RCLike.sqrt_normSq_eq_norm, NumberField.FinitePlace.norm_embedding', MonoidWithZeroHom.snd_apply_coe, MonoidWithZero.inverse_apply, Cardinal.toNat_add, Ideal.absNorm_relNorm, Valuation.restrict_exists_div_eq, RCLike.normSq_apply, Int.absNorm_under_eq_sInf, Ideal.absNorm_span_singleton, Valuation.IsEquiv.orderMonoidIso_spec, FractionalIdeal.coeIdeal_absNorm, Valuation.RankOne.hom_eq_zero_iff, lcm_units_coe_right, Quaternion.im_sq, Ideal.absNorm_algebraMap, Multiset.normalize_gcd, Valued.isClopen_closedBall, Valuation.RankOne.restrict_RankOne_hom_eq, AbsoluteValue.coe_toMonoidWithZeroHom, LinearOrderedCommGroupWithZero.inl_apply, Int.cast_mem_ideal_iff, LinearOrderedCommGroupWithZero.inr_apply, Ideal.relNorm_map_algEquiv, normalize_associated, OrderMonoidWithZeroHom.coe_monoidWithZeroHom, FractionalIdeal.absNorm_eq_zero_iff, MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid, RCLike.normSq_one, Ideal.span_singleton_absNorm_le, Polynomial.monic_normalize, Real.nndist_eq', Ideal.natAbs_det_basis_change, Perfection.teichmuller₀_mapMonoidHom_idealQuotientMk, Valuation.RankLeOne.strictMono', Multiset.gcd_map_mul, NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, Quaternion.normSq_div, Valuation.exists_setOf_restrict_le_iff, MonoidWithZeroHom.inr_injective, Ideal.ringChar_quot, Complex.normSq_neg, Real.exists_lt_of_strictMono, WithZero.map'_id, MonoidWithZeroHom.commute_inl_inr, MonoidWithZeroHom.fst_comp_inr, NumberField.mixedEmbedding.norm_negAt, normalize_zero, NumberField.mixedEmbedding.norm_unit, Int.liesOver_span_absNorm, UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors, IsValuativeTopology.isOpen_sphere, Quaternion.normSq_star, UpperHalfPlane.c_mul_im_sq_le_normSq_denom, Cardinal.zero_toNat, ValuationSubring.mapOfLE_comp_valuation, MonoidWithZeroHom.ext_int_iff, normalize_idem, Complex.range_normSq, Quaternion.normSq_ratCast, NumberField.FinitePlace.norm_embedding_int, UpperHalfPlane.smulAux'_im, Finset.normalize_gcd, lcm_eq_normalize, Quaternion.continuous_normSq, MonoidWithZeroHom.ValueGroup₀.embedding_strictMono, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, Complex.normSq_ofReal_sub_I_mul_sqrt_one_sub, Cardinal.aleph_toNat, Ideal.relNorm_eq_pow_of_isMaximal, Cardinal.natCast_toNat_le, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, Complex.normSq_eq_zero, RCLike.normSq_sub, Submonoid.LocalizationMap.lift₀_def, Nat.absNorm_under_prime, IsValuativeTopology.isClopen_closedBall, Valuation.mem_nhds_iff, GaussianInt.normSq_div_sub_div_lt_one, Int.nonneg_iff_normalize_eq_self, MonoidWithZeroHom.ENatMap_apply, normalize_eq_normalize_iff_associated, GaussianInt.intCast_complex_norm, NumberField.FinitePlace.norm_def, EulerProduct.exp_tsum_primes_log_eq_tsum, PowerSeries.X_eq_normalizeX, Quaternion.normSq_coe, MonoidWithZeroHom.inl_apply_unit, Ideal.relNorm_comap_algEquiv, Valuation.is_topological_valuation, Cardinal.toNat_eq_ofNat, Real.cast_natAbs_eq_nnabs_cast, Cardinal.one_toNat, normalize_associated_iff, Polynomial.X_eq_normalize, MonoidWithZeroHom.snd_surjective, Valuation.isClopen_sphere, Cardinal.continuum_toNat, Polynomial.content_monomial, MonoidWithZeroHom.toZeroHom_injective, Polynomial.map_normalize, normalize_eq, NumberField.mixedEmbedding.norm_apply, Valuation.isClosed_sphere, RCLike.normSq_conj, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, RCLike.inv_re, Complex.normSq_one, NumberField.mixedEmbedding.normAtPlace_real, MulEquiv.toMonoidWithZeroHom_surjective, lcm_one_right, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, Valued.extensionValuation_toFun, WithZero.map'_injective_iff, Ideal.absNorm_dvd_norm_of_mem, Perfection.teichmullerFun_eq_teichmuller₀, associated_normalize, WithZero.map'_map', FractionalIdeal.absNorm_one
MonoidWithZeroHomClass 📖	CompData	10 math math: OrderMonoidWithZeroHom.instMonoidWithZeroHomClass, ValuationClass.toMonoidWithZeroHomClass, MonoidWithZeroHom.monoidWithZeroHomClass, NumberField.InfinitePlace.instMonoidWithZeroHomClassReal, RingHomClass.toMonoidWithZeroHomClass, AbsoluteValue.monoidWithZeroHomClass, Submonoid.instMonoidWithZeroHomClassLocalizationMap, MulEquivClass.toMonoidWithZeroHomClass, NumberField.FinitePlace.instMonoidWithZeroHomClassReal, MulRingSeminormClass.toMonoidWithZeroHomClass
instCoeTCMonoidWithZeroHomOfMonoidWithZeroHomClass 📖	CompOp	—
powMonoidWithZeroHom 📖	CompOp	2 math math: powMonoidWithZeroHom_apply, coe_powMonoidWithZeroHom
«term_→*₀_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_powMonoidWithZeroHom 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MonoidWithZeroHom.funLike powMonoidWithZeroHom Monoid.toPow MonoidWithZero.toMonoid	—	—
powMonoidWithZeroHom_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MonoidWithZeroHom.funLike powMonoidWithZeroHom Monoid.toPow MonoidWithZero.toMonoid	—	—

---

← Back to Index