Basic

📁 Source: Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean

Statistics

Metric	Count
Definitions InfinitePlace, IsComplex, IsReal, fintype, embedding, embedding_of_isReal, instFunLikeReal, mk, mkComplex, mkReal, mult, nrComplexPlaces, nrRealPlaces, IsInfinitePlace, infinitePlace	15
Theorems conjugate_sign, nrRealPlaces_eq_zero_of_two_lt, apply, card_add_two_mul_card_eq_rank, card_complex_embeddings, card_eq_nrRealPlaces_add_nrComplexPlaces, card_filter_mk_eq, card_real_embeddings, coe_apply, conjugate_embedding_eq_of_isReal, conjugate_embedding_injective, denseRange_algebraMap_pi, disjoint_isReal_isComplex, embedding_inj, embedding_injective, embedding_mk_eq, embedding_mk_eq_of_isReal, embedding_of_isReal_apply, eq_iff_eq, eq_iff_isEquiv, eq_of_embedding_eq_conjugate, eq_one_of_rpow_eq, ext, ext_iff, instMonoidWithZeroHomClassReal, instNonnegHomClassReal, isComplex_iff, isComplex_mk_iff, isInfinitePlace, isNontrivial, isReal_iff, isReal_mk_iff, isReal_of_mk_isReal, isReal_or_isComplex, le_iff_le, map_intCast, map_natCast, map_ratCast, mkComplex_coe, mkReal_coe, mk_conjugate_eq, mk_embedding, mk_eq_iff, mult_coe_ne_zero, mult_isComplex, mult_isReal, mult_ne_zero, mult_pos, ne_of_isReal_isComplex, norm_embedding_eq, norm_embedding_of_isReal, not_isComplex_iff_isReal, not_isReal_iff_isComplex, not_isReal_of_mk_isComplex, nrComplexPlaces_eq_zero_of_finrank_eq_one, nrRealPlaces_eq_one_of_finrank_eq_one, nrRealPlaces_pos_of_odd_finrank, one_le_mult, one_le_of_lt_one, pos_iff, prod_eq_abs_norm, prod_eq_prod_mul_prod, sum_eq_sum_add_sum, sum_mult_eq, adjoin_eq_top_of_infinitePlace_lt, instNonemptyInfinitePlaceOfRingHomComplex, isInfinitePlace_iff, is_primitive_element_of_infinitePlace_lt, infinitePlace_apply, instSubsingletonInfinitePlace, isReal_infinitePlace	71
Total	86

NumberField

Definitions

Name	Category	Theorems
InfinitePlace 📖	CompOp	349 math math: InfinitePlace.mult_isComplex, mixedEmbedding.integral_comp_polarSpaceCoord_symm, mixedEmbedding.fundamentalCone.expMapBasis_apply', mixedEmbedding.fundamentalDomain_integerLattice, mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, mixedEmbedding.logMap_one, mixedEmbedding.lintegral_comp_polarCoord_symm, InfinitePlace.norm_embedding_of_isReal, mixedEmbedding.fundamentalCone.interior_paramSet, mixedEmbedding.measurable_polarCoordReal_symm, Units.finrank_eq_rank, InfinitePlace.sum_mult_eq, mixedEmbedding.norm_eq_sup'_normAtPlace, Units.logEmbedding_fundSystem, mixedEmbedding.convexBodyLT'_mem, mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, InfinitePlace.le_iff_le, mixedEmbedding.convexBodySumFun_add_le, InfinitePlace.nat_card_stabilizer_eq_one_or_two, InfinitePlace.isUnramified_iff_card_stabilizer_eq_one, IsCMField.equivInfinitePlace_symm_apply, instNonemptyInfinitePlaceOfRingHomComplex, mixedEmbedding.normAtAllPlaces_apply, mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, mixedEmbedding.normAtPlace_polarCoord_symm_of_isComplex, mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, mixedEmbedding.norm_unit_smul, mixedEmbedding.norm_eq_norm, mixedEmbedding.norm_le_convexBodySumFun, mixedEmbedding.mem_idealLattice, mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, Units.regOfFamily_eq_det, InfinitePlace.exists_smul_eq_of_comap_eq, Units.dirichletUnitTheorem.seq_decreasing, mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, InfinitePlace.card_mono, mixedEmbedding.fundamentalCone.compactSet_eq_union_aux₁, mixedEmbedding.polarCoordReal_apply, InfinitePlace.IsUnramified.stabilizer_eq_bot, mixedEmbedding.commMap_apply_of_isComplex, Units.pos_at_place, InfinitePlace.Completion.norm_coe, InfinitePlace.comap_apply, mixedEmbedding.instNoAtomsMixedSpaceVolume, prod_abs_eq_one, InfinitePlace.card_stabilizer, mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, mixedEmbedding.convexBodyLT_volume, InfinitePlace.smul_apply, mixedEmbedding.polarSpaceCoord_target, mixedEmbedding.negAt_apply_snd, Units.dirichletUnitTheorem.seq_next, mixedEmbedding.convexBodyLT_mem, InfinitePlace.coe_apply, ComplexEmbedding.IsConj.coe_stabilizer_mk, mixedEmbedding.convexBodySumFun_apply', mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, InfinitePlace.comp_of_comap_eq, mixedEmbedding.fundamentalCone.expMap_target, mixedEmbedding.convexBodySum_neg_mem, mixedEmbedding.negAt_preimage, mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, mixedEmbedding.iUnion_negAt_plusPart_ae, mixedEmbedding.normAtPlace_apply_of_isReal, mixedEmbedding.exists_primitive_element_lt_of_isComplex, mixedEmbedding.stdBasis_apply_isComplex_snd, mixedEmbedding.fundamentalCone.isCompact_compactSet, mixedEmbedding.negAt_signSet_apply_isComplex, mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, InfinitePlace.conjugate_embedding_injective, InfinitePlace.norm_embedding_eq, mixedEmbedding.fundamentalCone.smul_mem_of_mem, mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, InfinitePlace.mkReal_coe, mixedEmbedding.fundamentalCone.logMap_expMapBasis, InfinitePlace.smul_eq_comap, InfinitePlace.smul_mk, Units.instZLattice_unitLattice, InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, mulHeight_eq, mixedEmbedding.convexBodySum_compact, Units.span_basisOfIsMaxRank, mixedEmbedding.fundamentalCone.norm_pos_of_mem, Units.logEmbeddingQuot_apply, InfinitePlace.pos_iff, Units.basisOfIsMaxRank_apply, mixedEmbedding.fundamentalCone.subset_interior_normLeOne, mixedEmbedding.negAt_signSet_apply_isReal, Units.regulator_eq_det, mixedEmbedding.fundamentalDomain_idealLattice, InfinitePlace.card_filter_mk_eq, mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_eq, Units.finrank_mul_regOfFamily_eq_det, mixedEmbedding.mem_span_fractionalIdealLatticeBasis, mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, mixedEmbedding.convexBodySumFun_apply, InfinitePlace.isUnramified_smul_iff, InfinitePlace.orbitRelEquiv_apply_mk'', InfinitePlace.card_eq_card_isUnramifiedIn, mixedEmbedding.polarCoordReal_source, mixedEmbedding.fundamentalCone.mem_normLeOne, InfinitePlace.map_ratCast, mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, InfinitePlace.ext_iff, mixedEmbedding.span_idealLatticeBasis, mixedEmbedding.fundamentalCone.norm_expMapBasis, mixedEmbedding.convexBodySumFun_smul, InfinitePlace.instMonoidWithZeroHomClassReal, mixedEmbedding.logMap_real_smul, mixedEmbedding.polarCoord_symm_apply, mixedEmbedding.indexEquiv_apply_isComplex_fst, Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, mixedEmbedding.unit_smul_eq_iff_mul_eq, IsCMField.equivInfinitePlace_apply, mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq, InfinitePlace.smul_coe_apply, mixedEmbedding.realSpace.volume_eq_zero, mixedEmbedding.mem_span_latticeBasis, Units.dirichletUnitTheorem.sum_logEmbedding_component, mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet, hermiteTheorem.finite_of_discr_bdd_of_isComplex, mixedEmbedding.euclidean.volumePreserving_toMixed, Units.dirichletUnitTheorem.unitLattice_span_eq_top, mixedEmbedding.covolume_idealLattice, mixedEmbedding.fundamentalCone.expMap_basis_of_eq, mixedEmbedding.volume_preserving_negAt, mixedEmbedding.normAtPlace_add_le, mixedEmbedding.fundamentalCone.prod_expMapBasis_pow, mixedEmbedding.negAt_apply_isComplex, mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet, mixedEmbedding.fundamentalCone.continuous_expMap, InfinitePlace.card_isUnramified, mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, mixedEmbedding.fundamentalCone.expMap_smul, InfinitePlace.isComplex_smul_iff, mixedEmbedding.adjust_f, Units.mem_torsion, mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, mixedEmbedding.mem_negAt_plusPart_of_mem, Units.regOfFamily_of_isMaxRank, mixedEmbedding.fundamentalCone.closure_normLeOne_subset, mixedEmbedding.convexBodySumFun_neg, IsCMField.card_infinitePlace_eq_card_infinitePlace, mixedEmbedding.convexBodySumFun_continuous, InfinitePlace.card_isUnramified_compl, mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, mixedEmbedding.logMap_eq_logEmbedding, mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, mixedEmbedding.fundamentalCone.hasFDerivAt_expMap, Units.dirichletUnitTheorem.mult_log_place_eq_zero, mixedEmbedding.norm_nonneg, mixedEmbedding.mixedEmbedding_apply_isReal, mixedEmbedding.stdBasis_apply_isComplex_fst, mixedEmbedding.fundamentalCone.continuous_expMapBasis, mixedEmbedding.norm_smul, mixedEmbedding.fundamentalDomain_stdBasis, mixedEmbedding.span_latticeBasis, mixedEmbedding.measurableSet_fundamentalCone, mixedEmbedding.fundamentalCone.expMap_symm_apply, Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, mixedEmbedding.polarCoord_source, InfinitePlace.isRamified_iff_card_stabilizer_eq_two, mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, mixedEmbedding.continuous_norm, Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, mixedEmbedding.det_matrixToStdBasis, mixedEmbedding.polarSpaceCoord_symm_apply, mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, mixedEmbedding.normAtAllPlaces_mixedEmbedding, mixedEmbedding.covolume_integerLattice, mixedEmbedding.mixedSpaceToRealMixedSpace_apply, Units.instDiscrete_unitLattice, mixedEmbedding.fundamentalCone.closure_paramSet, mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, mixedEmbedding.convexBodyLT_neg_mem, mixedEmbedding.polarCoord_target, mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis, mixedEmbedding.normAtPlace_polarCoord_symm_of_isReal, mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, mixedEmbedding.negAt_symm, InfinitePlace.denseRange_algebraMap_pi, mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem, InfinitePlace.isReal_smul_iff, mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp, mixedEmbedding.polarCoord_symm_eq, mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, Units.abs_det_eq_abs_det, mixedEmbedding.polarSpaceCoord_target', mixedEmbedding.exists_primitive_element_lt_of_isReal, mixedEmbedding.convexBodyLT'_volume, InfinitePlace.sum_eq_sum_add_sum, mixedEmbedding.iUnion_negAt_plusPart_union, mixedEmbedding.logMap_unit_smul, mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, mixedEmbedding.normAtPlace_neg, mixedEmbedding.unitSMul_smul, mixedEmbedding.continuous_normAtPlace, mixedEmbedding.indexEquiv_apply_isReal, mixedEmbedding.injective_mixedSpaceOfRealSpace, mixedEmbedding.fundamentalCone.expMapBasis_pos, mixedEmbedding.normAtPlace_apply, mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, mixedEmbedding.volume_eq_zero, mixedEmbedding.fundamentalCone.expMap_apply, mixedEmbedding.stdBasis_apply_isReal, mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, mixedEmbedding.normAtPlace_apply_of_isComplex, mixedEmbedding_injective, InfinitePlace.comap_smul, InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two, mixedEmbedding.forall_normAtPlace_eq_zero_iff, mixedEmbedding.convexBodyLT_convex, mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, Units.dirichletUnitTheorem.logEmbedding_component, InfinitePlace.mult_isReal, mixedEmbedding.logMap_apply, mixedEmbedding.fundamentalCone.injective_expMapBasis, Units.logEmbeddingQuot_injective, mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, mixedEmbedding.latticeBasis_apply, mixedEmbedding.unit_smul_eq_zero, InfinitePlace.isUnramified_iff_stabilizer_eq_bot, mixedEmbedding.lintegral_comp_polarCoordReal_symm, mixedEmbedding.measurable_polarCoord_symm, mixedEmbedding.fundamentalCone.intNorm_coe, mixedEmbedding.norm_eq_zero_iff, mixedEmbedding.fundamentalCone.expMap_source, mixedEmbedding.fundamentalCone.expMapBasis_apply'', mixedEmbedding.normAtPlace_nonneg, mixedEmbedding.logMap_real, mixedEmbedding.commMap_apply_of_isReal, Rat.infinitePlace_apply, mixedEmbedding.polarCoord_apply, mixedEmbedding.hasFDerivAt_polarCoordReal_symm, mixedEmbedding.continuous_normAtAllPlaces, mixedEmbedding.latticeBasis_repr_apply, mixedEmbedding.normAtPlace_negAt, mixedEmbedding.homeoRealMixedSpacePolarSpace_apply, mixedEmbedding.normAtPlace_smul, mixedEmbedding.fundamentalCone.isBounded_normLeOne, mixedEmbedding.finrank, IsUnramifiedAtInfinitePlaces.card_infinitePlace, mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, mixedEmbedding.fractionalIdealLatticeBasis_apply, mixedEmbedding.convexBodySum_isBounded, mixedEmbedding.polarSpaceCoord_apply, mixedEmbedding.negAt_apply_norm_isReal, mixedEmbedding.fundamentalCone.expMap_add, InfinitePlace.embedding_injective, InfinitePlace.mem_stabilizer_mk_iff, InfinitePlace.prod_eq_prod_mul_prod, InfinitePlace.mkComplex_coe, mixedEmbedding.fundamentalCone.expMapBasis_apply, Units.unitLattice_rank, InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces, mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_snd, mixedEmbedding.norm_real, mixedEmbedding.volume_fundamentalDomain_latticeBasis, Units.logEmbeddingEquiv_apply, mixedEmbedding.polarSpaceCoord_source, InfinitePlace.mem_orbit_iff, mixedEmbedding.indexEquiv_apply_isComplex_snd, InfinitePlace.eq_iff_eq, mixedEmbedding.polarCoord_target_eq_polarCoordReal_target, InfinitePlace.map_intCast, mixedEmbedding.fundamentalCone.compactSet_ae, mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, mixedEmbedding.euclidean.finrank, mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, mixedEmbedding.homeoRealMixedSpacePolarSpace_symm_apply, mixedEmbedding.euclidean.volumePreserving_toMixed_symm, mixedEmbedding.convexBodySum_convex, mixedEmbedding.fundamentalCone.mem_idealSet, mixedEmbedding.fundamentalCone.volume_normLeOne, IsCMField.infinitePlace_complexConj, prod_archAbsVal_eq, mixedEmbedding.fundamentalCone.zero_mem_compactSet, mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, mixedEmbedding.fundamentalCone.normAtAllPlaces_image_preimage_expMapBasis, mixedEmbedding.mixedEmbedding_apply_isComplex, mixedEmbedding.fundamentalCone.smul_mem_iff_mem, mixedEmbedding.fundamentalCone.mem_integerSet, mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, mixedEmbedding.det_fderivPolarCoordRealSymm, mixedEmbedding.fundamentalCone.expMap_sum, Units.finrank_mul_regulator_eq_det, InfinitePlace.prod_eq_abs_norm, mulHeight₁_eq, mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne_eq_image, mixedEmbedding.disjoint_span_commMap_ker, InfinitePlace.map_natCast, Units.sum_mult_mul_log, InfiniteAdeleRing.ringEquiv_mixedSpace_apply, mixedEmbedding.convexBodySum_volume, mixedEmbedding.convexBodyLT'_neg_mem, Units.regulator_eq_det', mixedEmbedding.polarCoordReal_target, Units.dirichletUnitTheorem.logEmbedding_ker, mixedEmbedding.fundamentalCone.expMapBasis_source, mixedEmbedding.logMap_zero, Units.dirichletUnitTheorem.exists_unit, mixedEmbedding.fundamentalCone.measurableSet_paramSet, mixedEmbedding.integral_comp_polarCoord_symm, mixedEmbedding.fundamentalCone.expMap_pos, mixedEmbedding.normAtComplexPlaces_apply_isComplex, InfinitePlace.comap_surjective, Units.basisOfIsMaxRank_fundSystem, mixedEmbedding.fundamentalCone.linearIndependent_completeFamily, mixedEmbedding.fundamentalCone.measurableSet_normLeOne, mixedEmbedding.commMap_canonical_eq_mixed, mixedEmbedding.norm_negAt, Rat.instSubsingletonInfinitePlace, mixedEmbedding.norm_unit, Units.regOfFamily_eq_det', mixedEmbedding.fundamentalCone.normLeOne_eq_preimage, InfinitePlace.apply, mixedEmbedding.integral_comp_polarCoordReal_symm, mixedEmbedding.fundamentalCone.compactSet_eq_union, mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, mixedEmbedding.measurable_polarSpaceCoord_symm, mixedEmbedding.nnnorm_eq_sup_normAtPlace, mixedEmbedding.fundamentalCone.injective_expMap, mixedEmbedding.fundamentalCone.expMap_basis_of_ne, mixedEmbedding.disjoint_negAt_plusPart, mixedEmbedding.logMap_mul, mixedEmbedding.volume_fundamentalDomain_stdBasis, mixedEmbedding.convexBodySum_mem, mixedEmbedding.fundamentalCone.expMapBasis_nonneg, mixedEmbedding.convexBodyLT'_convex, mixedEmbedding.mem_rat_span_latticeBasis, mixedEmbedding.norm_apply, mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, mixedEmbedding.normAtAllPlaces_normAtAllPlaces, mixedEmbedding.normAtPlace_real, mixedEmbedding.normAtComplexPlaces_apply_isReal, InfinitePlace.instNonnegHomClassReal, mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, hermiteTheorem.finite_of_discr_bdd_of_isReal, mixedEmbedding.mixedSpaceOfRealSpace_apply, mixedEmbedding.convexBodySumFun_eq_zero_iff, mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior, mixedEmbedding.lintegral_comp_polarSpaceCoord_symm
IsInfinitePlace 📖	MathDef	3 math math: isInfinitePlace_iff, InfinitePlace.isInfinitePlace, mem_multisetInfinitePlace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_eq_top_of_infinitePlace_lt 📖	mathematical	Real Real.instLT DFunLike.coe InfinitePlace InfinitePlace.instFunLikeReal RingOfIntegers.val Real.instOne InfinitePlace.IsReal abs Real.lattice Real.instAddGroup Complex.re RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring RingHom.instFunLike InfinitePlace.embedding	Algebra.adjoin Rat.commSemiring DivisionRing.toRatAlgebra Field.toDivisionRing to_charZero Set Set.instSingletonSet Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	to_charZero IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic IsAlgebraic.of_finite Rat.nontrivial to_finiteDimensional is_primitive_element_of_infinitePlace_lt
instNonemptyInfinitePlaceOfRingHomComplex 📖	mathematical	—	InfinitePlace	—	Set.instNonemptyRange Complex.instNontrivial
isInfinitePlace_iff 📖	mathematical	—	IsInfinitePlace AbsoluteValue Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial	—	Complex.instNontrivial InfinitePlace.isInfinitePlace
is_primitive_element_of_infinitePlace_lt 📖	mathematical	Real Real.instLT DFunLike.coe InfinitePlace InfinitePlace.instFunLikeReal RingOfIntegers.val Real.instOne InfinitePlace.IsReal abs Real.lattice Real.instAddGroup Complex.re RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring RingHom.instFunLike InfinitePlace.embedding	IntermediateField.adjoin Rat.instField DivisionRing.toRatAlgebra Field.toDivisionRing to_charZero Set Set.instSingletonSet Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	to_charZero Complex.instCharZero Field.primitive_element_iff_algHom_eq_of_eval to_finiteDimensional Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite Rat.nontrivial PerfectField.ofCharZero Rat.instCharZero IsAlgClosed.splits Complex.isAlgClosed InfinitePlace.one_le_of_lt_one Mathlib.Tactic.Contrapose.contrapose₁ InfinitePlace.norm_embedding_eq InfinitePlace.conjugate_embedding_eq_of_isReal InfinitePlace.mk_eq_iff InfinitePlace.mk_embedding LT.lt.not_ge Complex.conj_eq_iff_im RingHom.congr_fun Complex.norm_real add_zero MulZeroClass.zero_mul Complex.ofReal_zero Complex.re_add_im

NumberField.InfinitePlace

Definitions

Name	Category	Theorems
IsComplex 📖	MathDef	218 math math: mult_isComplex, NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.logMap_one, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, NumberField.mixedEmbedding.measurable_polarCoordReal_symm, NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, NumberField.mixedEmbedding.convexBodyLT'_mem, NumberField.mixedEmbedding.convexBodySumFun_add_le, isReal_or_isComplex, not_isComplex_iff_isReal, NumberField.mixedEmbedding.normAtAllPlaces_apply, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, NumberField.mixedEmbedding.norm_unit_smul, NumberField.mixedEmbedding.norm_eq_norm, NumberField.mixedEmbedding.norm_le_convexBodySumFun, NumberField.mixedEmbedding.mem_idealLattice, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, NumberField.mixedEmbedding.polarCoordReal_apply, IsRamified.isComplex, NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, NumberField.mixedEmbedding.convexBodyLT_volume, NumberField.mixedEmbedding.polarSpaceCoord_target, NumberField.mixedEmbedding.negAt_apply_snd, NumberField.mixedEmbedding.convexBodyLT_mem, NumberField.mixedEmbedding.convexBodySumFun_apply', NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, NumberField.mixedEmbedding.convexBodySum_neg_mem, NumberField.mixedEmbedding.negAt_preimage, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, NumberField.mixedEmbedding.normAtPlace_apply_of_isReal, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, NumberField.mixedEmbedding.convexBodySum_compact, NumberField.mixedEmbedding.fundamentalCone.norm_pos_of_mem, NumberField.mixedEmbedding.fundamentalCone.subset_interior_normLeOne, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, NumberField.mixedEmbedding.convexBodySumFun_apply, NumberField.mixedEmbedding.polarCoordReal_source, NumberField.mixedEmbedding.fundamentalCone.mem_normLeOne, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, NumberField.mixedEmbedding.span_idealLatticeBasis, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, NumberField.mixedEmbedding.convexBodySumFun_smul, NumberField.mixedEmbedding.logMap_real_smul, NumberField.mixedEmbedding.polarCoord_symm_apply, NumberField.mixedEmbedding.indexEquiv_apply_isComplex_fst, NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq, NumberField.mixedEmbedding.mem_span_latticeBasis, NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.mixedEmbedding.volume_preserving_negAt, NumberField.mixedEmbedding.normAtPlace_add_le, NumberField.mixedEmbedding.negAt_apply_isComplex, isRamified_iff, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, isComplex_smul_iff, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, NumberField.mixedEmbedding.fundamentalCone.closure_normLeOne_subset, NumberField.mixedEmbedding.convexBodySumFun_neg, NumberField.mixedEmbedding.convexBodySumFun_continuous, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.logMap_eq_logEmbedding, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, NumberField.mixedEmbedding.norm_nonneg, NumberField.mixedEmbedding.mixedEmbedding_apply_isReal, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, NumberField.mixedEmbedding.norm_smul, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, NumberField.mixedEmbedding.span_latticeBasis, NumberField.IsTotallyComplex.isComplex, NumberField.mixedEmbedding.measurableSet_fundamentalCone, NumberField.mixedEmbedding.polarCoord_source, NumberField.isTotallyComplex_iff, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, NumberField.mixedEmbedding.continuous_norm, NumberField.mixedEmbedding.det_matrixToStdBasis, NumberField.mixedEmbedding.polarSpaceCoord_symm_apply, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding, NumberField.mixedEmbedding.covolume_integerLattice, NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace_apply, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, NumberField.mixedEmbedding.convexBodyLT_neg_mem, NumberField.mixedEmbedding.polarCoord_target, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isReal, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, not_isUnramified_iff, isUnramified_iff, NumberField.mixedEmbedding.negAt_symm, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, NumberField.mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem, NumberField.mixedEmbedding.polarCoord_symm_eq, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, NumberField.mixedEmbedding.polarSpaceCoord_target', NumberField.mixedEmbedding.convexBodyLT'_volume, sum_eq_sum_add_sum, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, NumberField.mixedEmbedding.normAtPlace_neg, NumberField.mixedEmbedding.unitSMul_smul, NumberField.mixedEmbedding.continuous_normAtPlace, NumberField.mixedEmbedding.indexEquiv_apply_isReal, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.normAtPlace_apply, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, NumberField.mixedEmbedding.volume_eq_zero, NumberField.mixedEmbedding.stdBasis_apply_isReal, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, NumberField.mixedEmbedding_injective, NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff, NumberField.mixedEmbedding.convexBodyLT_convex, isComplex_iff, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, NumberField.mixedEmbedding.logMap_apply, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, NumberField.mixedEmbedding.latticeBasis_apply, NumberField.mixedEmbedding.unit_smul_eq_zero, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, NumberField.mixedEmbedding.measurable_polarCoord_symm, NumberField.mixedEmbedding.fundamentalCone.intNorm_coe, NumberField.mixedEmbedding.norm_eq_zero_iff, NumberField.mixedEmbedding.normAtPlace_nonneg, NumberField.mixedEmbedding.logMap_real, NumberField.mixedEmbedding.commMap_apply_of_isReal, NumberField.mixedEmbedding.polarCoord_apply, NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, NumberField.mixedEmbedding.continuous_normAtAllPlaces, NumberField.mixedEmbedding.latticeBasis_repr_apply, NumberField.mixedEmbedding.normAtPlace_negAt, not_isReal_iff_isComplex, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply, NumberField.mixedEmbedding.normAtPlace_smul, NumberField.mixedEmbedding.fundamentalCone.isBounded_normLeOne, NumberField.mixedEmbedding.finrank, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, NumberField.mixedEmbedding.convexBodySum_isBounded, NumberField.mixedEmbedding.polarSpaceCoord_apply, NumberField.mixedEmbedding.negAt_apply_norm_isReal, prod_eq_prod_mul_prod, mkComplex_coe, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_snd, NumberField.mixedEmbedding.norm_real, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, NumberField.mixedEmbedding.polarSpaceCoord_source, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, NumberField.mixedEmbedding.indexEquiv_apply_isComplex_snd, NumberField.mixedEmbedding.polarCoord_target_eq_polarCoordReal_target, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, NumberField.mixedEmbedding.euclidean.finrank, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_symm_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, NumberField.mixedEmbedding.convexBodySum_convex, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, NumberField.mixedEmbedding.mixedEmbedding_apply_isComplex, NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, NumberField.mixedEmbedding.disjoint_span_commMap_ker, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, NumberField.mixedEmbedding.convexBodySum_volume, NumberField.mixedEmbedding.convexBodyLT'_neg_mem, NumberField.mixedEmbedding.polarCoordReal_target, isComplex_mk_iff, NumberField.mixedEmbedding.logMap_zero, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isComplex, NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne, NumberField.mixedEmbedding.commMap_canonical_eq_mixed, NumberField.mixedEmbedding.norm_negAt, NumberField.mixedEmbedding.norm_unit, disjoint_isReal_isComplex, NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, NumberField.mixedEmbedding.disjoint_negAt_plusPart, NumberField.mixedEmbedding.logMap_mul, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, NumberField.mixedEmbedding.convexBodySum_mem, NumberField.mixedEmbedding.convexBodyLT'_convex, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, NumberField.mixedEmbedding.norm_apply, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, NumberField.mixedEmbedding.normAtPlace_real, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm
IsReal 📖	MathDef	215 math math: NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.logMap_one, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, NumberField.mixedEmbedding.measurable_polarCoordReal_symm, NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, NumberField.mixedEmbedding.convexBodyLT'_mem, NumberField.mixedEmbedding.convexBodySumFun_add_le, isReal_or_isComplex, not_isComplex_iff_isReal, NumberField.mixedEmbedding.normAtAllPlaces_apply, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isComplex, NumberField.mixedEmbedding.norm_unit_smul, NumberField.mixedEmbedding.norm_eq_norm, NumberField.mixedEmbedding.norm_le_convexBodySumFun, NumberField.mixedEmbedding.mem_idealLattice, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, NumberField.mixedEmbedding.polarCoordReal_apply, NumberField.mixedEmbedding.commMap_apply_of_isComplex, NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, NumberField.mixedEmbedding.convexBodyLT_volume, NumberField.mixedEmbedding.polarSpaceCoord_target, NumberField.mixedEmbedding.negAt_apply_snd, NumberField.mixedEmbedding.convexBodyLT_mem, NumberField.mixedEmbedding.convexBodySumFun_apply', NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, NumberField.mixedEmbedding.convexBodySum_neg_mem, NumberField.mixedEmbedding.negAt_preimage, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, isReal_iff, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, mkReal_coe, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, Rat.isReal_infinitePlace, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, NumberField.mixedEmbedding.convexBodySum_compact, NumberField.mixedEmbedding.fundamentalCone.norm_pos_of_mem, NumberField.mixedEmbedding.fundamentalCone.subset_interior_normLeOne, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, NumberField.mixedEmbedding.convexBodySumFun_apply, NumberField.mixedEmbedding.polarCoordReal_source, NumberField.mixedEmbedding.fundamentalCone.mem_normLeOne, NumberField.mixedEmbedding.span_idealLatticeBasis, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, NumberField.mixedEmbedding.convexBodySumFun_smul, NumberField.mixedEmbedding.logMap_real_smul, NumberField.mixedEmbedding.polarCoord_symm_apply, NumberField.mixedEmbedding.indexEquiv_apply_isComplex_fst, NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq, NumberField.mixedEmbedding.mem_span_latticeBasis, NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.mixedEmbedding.volume_preserving_negAt, NumberField.mixedEmbedding.normAtPlace_add_le, NumberField.mixedEmbedding.negAt_apply_isComplex, isRamified_iff, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, IsRamified.isReal, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, NumberField.mixedEmbedding.fundamentalCone.closure_normLeOne_subset, NumberField.isTotallyReal_iff, NumberField.mixedEmbedding.convexBodySumFun_neg, NumberField.mixedEmbedding.convexBodySumFun_continuous, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.logMap_eq_logEmbedding, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, isReal_mk_iff, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, NumberField.mixedEmbedding.norm_nonneg, NumberField.mixedEmbedding.mixedEmbedding_apply_isReal, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, NumberField.mixedEmbedding.norm_smul, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, NumberField.mixedEmbedding.span_latticeBasis, NumberField.mixedEmbedding.measurableSet_fundamentalCone, NumberField.mixedEmbedding.polarCoord_source, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, NumberField.mixedEmbedding.continuous_norm, NumberField.mixedEmbedding.det_matrixToStdBasis, NumberField.mixedEmbedding.polarSpaceCoord_symm_apply, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding, NumberField.mixedEmbedding.covolume_integerLattice, NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace_apply, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, NumberField.mixedEmbedding.convexBodyLT_neg_mem, NumberField.mixedEmbedding.polarCoord_target, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, not_isUnramified_iff, isUnramified_iff, NumberField.mixedEmbedding.negAt_symm, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, NumberField.mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem, isReal_smul_iff, NumberField.mixedEmbedding.polarCoord_symm_eq, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, NumberField.mixedEmbedding.polarSpaceCoord_target', NumberField.mixedEmbedding.convexBodyLT'_volume, sum_eq_sum_add_sum, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, NumberField.mixedEmbedding.normAtPlace_neg, isReal_comap_iff, NumberField.mixedEmbedding.unitSMul_smul, NumberField.mixedEmbedding.continuous_normAtPlace, NumberField.mixedEmbedding.indexEquiv_apply_isReal, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.normAtPlace_apply, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, NumberField.mixedEmbedding.volume_eq_zero, NumberField.mixedEmbedding.stdBasis_apply_isReal, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex, NumberField.mixedEmbedding_injective, NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff, NumberField.mixedEmbedding.convexBodyLT_convex, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, mult_isReal, NumberField.mixedEmbedding.logMap_apply, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, NumberField.mixedEmbedding.latticeBasis_apply, NumberField.mixedEmbedding.unit_smul_eq_zero, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, NumberField.mixedEmbedding.measurable_polarCoord_symm, NumberField.mixedEmbedding.fundamentalCone.intNorm_coe, NumberField.mixedEmbedding.norm_eq_zero_iff, NumberField.mixedEmbedding.normAtPlace_nonneg, NumberField.mixedEmbedding.logMap_real, NumberField.mixedEmbedding.polarCoord_apply, NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, NumberField.mixedEmbedding.continuous_normAtAllPlaces, NumberField.mixedEmbedding.latticeBasis_repr_apply, NumberField.mixedEmbedding.normAtPlace_negAt, not_isReal_iff_isComplex, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply, NumberField.mixedEmbedding.normAtPlace_smul, NumberField.mixedEmbedding.fundamentalCone.isBounded_normLeOne, NumberField.mixedEmbedding.finrank, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, NumberField.mixedEmbedding.convexBodySum_isBounded, NumberField.mixedEmbedding.polarSpaceCoord_apply, NumberField.mixedEmbedding.negAt_apply_norm_isReal, prod_eq_prod_mul_prod, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_snd, NumberField.mixedEmbedding.norm_real, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, NumberField.mixedEmbedding.polarSpaceCoord_source, NumberField.mixedEmbedding.indexEquiv_apply_isComplex_snd, NumberField.mixedEmbedding.polarCoord_target_eq_polarCoordReal_target, NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, NumberField.mixedEmbedding.euclidean.finrank, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_symm_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, NumberField.mixedEmbedding.convexBodySum_convex, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, NumberField.mixedEmbedding.mixedEmbedding_apply_isComplex, NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, NumberField.mixedEmbedding.disjoint_span_commMap_ker, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, NumberField.mixedEmbedding.convexBodySum_volume, NumberField.mixedEmbedding.convexBodyLT'_neg_mem, NumberField.mixedEmbedding.polarCoordReal_target, NumberField.mixedEmbedding.logMap_zero, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne, NumberField.mixedEmbedding.commMap_canonical_eq_mixed, NumberField.IsTotallyReal.isReal, NumberField.mixedEmbedding.norm_negAt, NumberField.mixedEmbedding.norm_unit, disjoint_isReal_isComplex, NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, NumberField.mixedEmbedding.disjoint_negAt_plusPart, NumberField.mixedEmbedding.logMap_mul, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, NumberField.mixedEmbedding.convexBodySum_mem, NumberField.mixedEmbedding.convexBodyLT'_convex, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, NumberField.mixedEmbedding.norm_apply, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, NumberField.mixedEmbedding.normAtPlace_real, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isReal, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm
embedding 📖	CompOp	31 math math: IsUnramified.isUnmixed, NumberField.mixedEmbedding.convexBodyLT'_mem, isometry_embedding, IsUnramified.isUnmixed_conjugate, NumberField.mixedEmbedding.commMap_apply_of_isComplex, IsRamified.isMixed_conjugate_embedding, conjugate_embedding_injective, norm_embedding_eq, isReal_iff, mk_embedding, IsRamified.comap_embedding_conjugate, NumberField.mixedEmbedding.indexEquiv_apply_isComplex_fst, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt', embedding_mk_eq_of_isReal, IsRamified.comap_embedding, LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq, embedding_of_isReal_apply, Completion.extensionEmbedding_coe, conjugate_embedding_eq_of_isReal, embedding_mk_eq, NumberField.mixedEmbedding.indexEquiv_apply_isReal, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt', isComplex_iff, LiesOver.mk_embedding_comp, NumberField.mixedEmbedding.commMap_apply_of_isReal, embedding_inj, embedding_injective, NumberField.mixedEmbedding.indexEquiv_apply_isComplex_snd, NumberField.mixedEmbedding.mixedEmbedding_apply_isComplex, comap_embedding_of_isReal, IsRamified.isMixed_embedding
embedding_of_isReal 📖	CompOp	6 math math: norm_embedding_of_isReal, Completion.extensionEmbeddingOfIsReal_coe, NumberField.mixedEmbedding.mixedEmbedding_apply_isReal, embedding_of_isReal_apply, isometry_embedding_of_isReal, Completion.extensionEmbedding_of_isReal_coe
instFunLikeReal 📖	CompOp	50 math math: NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', norm_embedding_of_isReal, NumberField.mixedEmbedding.convexBodyLT'_mem, le_iff_le, NumberField.IsCMField.equivInfinitePlace_symm_apply, NumberField.Units.regOfFamily_eq_det, NumberField.Units.dirichletUnitTheorem.seq_decreasing, NumberField.Units.pos_at_place, Completion.norm_coe, comap_apply, NumberField.prod_abs_eq_one, smul_apply, NumberField.Units.dirichletUnitTheorem.seq_next, NumberField.mixedEmbedding.convexBodyLT_mem, coe_apply, comp_of_comap_eq, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, norm_embedding_eq, NumberField.mulHeight_eq, pos_iff, NumberField.Units.regulator_eq_det, NumberField.Units.finrank_mul_regOfFamily_eq_det, map_ratCast, ext_iff, instMonoidWithZeroHomClassReal, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, NumberField.Units.mem_torsion, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt', NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt, NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding, NumberField.Units.abs_det_eq_abs_det, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt, NumberField.mixedEmbedding.normAtPlace_apply, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt', NumberField.Units.dirichletUnitTheorem.logEmbedding_component, Rat.infinitePlace_apply, eq_iff_eq, map_intCast, NumberField.IsCMField.infinitePlace_complexConj, NumberField.Units.finrank_mul_regulator_eq_det, prod_eq_abs_norm, NumberField.mulHeight₁_eq, map_natCast, NumberField.Units.sum_mult_mul_log, NumberField.Units.dirichletUnitTheorem.exists_unit, apply, instNonnegHomClassReal
mk 📖	CompOp	—
mkComplex 📖	CompOp	1 math math: mkComplex_coe
mkReal 📖	CompOp	1 math math: mkReal_coe
mult 📖	CompOp	42 math math: mult_isComplex, sum_mult_eq, NumberField.Units.regOfFamily_eq_det, NumberField.prod_abs_eq_one, NumberField.mixedEmbedding.convexBodyLT_volume, NumberField.mulHeight_eq, NumberField.Units.regulator_eq_det, card_filter_mk_eq, NumberField.Units.finrank_mul_regOfFamily_eq_det, NumberField.mixedEmbedding.convexBodySumFun_apply, NumberField.IsTotallyComplex.mult_eq, NumberField.IsTotallyReal.mult_eq, mult_comap_le, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow, NumberField.mixedEmbedding.adjust_f, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, NumberField.mixedEmbedding.logMap_apply_of_norm_eq_one, IsUnramified.eq, NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, NumberField.mixedEmbedding.fundamentalCone.expMap_symm_apply, NumberField.count_multisetInfinitePlace_eq_mult, NumberField.Units.abs_det_eq_abs_det, NumberField.mixedEmbedding.convexBodyLT'_volume, NumberField.mixedEmbedding.fundamentalCone.expMap_single_symm_apply, NumberField.mixedEmbedding.fundamentalCone.expMap_apply, mult_pos, one_le_mult, NumberField.Units.dirichletUnitTheorem.logEmbedding_component, mult_isReal, NumberField.mixedEmbedding.logMap_apply, NumberField.mixedEmbedding.logMap_apply_of_norm_one, NumberField.mixedEmbedding.fundamentalCone.expMap_single_apply, NumberField.prod_archAbsVal_eq, isUnramified_iff_mult_le, NumberField.Units.finrank_mul_regulator_eq_det, prod_eq_abs_norm, NumberField.mulHeight₁_eq, NumberField.Units.sum_mult_mul_log, NumberField.mixedEmbedding.convexBodySum_mem, NumberField.mixedEmbedding.norm_apply
nrComplexPlaces 📖	CompOp	28 math math: NumberField.dedekindZeta_residue_def, NumberField.abs_discr_ge', IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two, NumberField.IsTotallyComplex.finrank, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, ComplexEmbedding.conjugate_sign, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.Ideal.tendsto_norm_le_div_atTop₀, NumberField.mixedEmbedding.det_matrixToStdBasis, NumberField.mixedEmbedding.covolume_integerLattice, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, NumberField.exists_ideal_in_class_of_norm_le, NumberField.Ideal.tendsto_norm_le_div_atTop, NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, NumberField.nrComplexPlaces_eq_zero_iff, nrComplexPlaces_eq_zero_of_finrank_eq_one, NumberField.sign_discr, card_eq_nrRealPlaces_add_nrComplexPlaces, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, card_add_two_mul_card_eq_rank, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, card_complex_embeddings, NumberField.IsTotallyReal.nrComplexPlaces_eq_zero
nrRealPlaces 📖	CompOp	17 math math: NumberField.dedekindZeta_residue_def, IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt, NumberField.IsTotallyReal.finrank, NumberField.nrRealPlaces_eq_zero_iff, NumberField.Ideal.tendsto_norm_le_div_atTop₀, card_real_embeddings, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, NumberField.Ideal.tendsto_norm_le_div_atTop, IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero, nrRealPlaces_pos_of_odd_finrank, card_eq_nrRealPlaces_add_nrComplexPlaces, card_add_two_mul_card_eq_rank, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, nrRealPlaces_eq_one_of_finrank_eq_one, NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart, NumberField.IsTotallyComplex.nrRealPlaces_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	mathematical	—	DFunLike.coe NumberField.InfinitePlace Real instFunLikeReal Norm.norm Complex Complex.instNorm RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring RingHom.instFunLike	—	—
card_add_two_mul_card_eq_rank 📖	mathematical	—	nrRealPlaces nrComplexPlaces Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	NumberField.to_charZero Complex.instCharZero card_real_embeddings card_complex_embeddings Fintype.card_subtype_compl NumberField.Embeddings.card Complex.isAlgClosed Fintype.card_subtype_le
card_complex_embeddings 📖	mathematical	—	Fintype.card RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring NumberField.ComplexEmbedding.IsReal Subtype.fintype NumberField.Embeddings.instFintypeRingHom Complex.instField Complex.instCharZero nrComplexPlaces	—	Complex.instCharZero Fintype.card_subtype Fintype.card_congr not_isReal_of_mk_isComplex mkComplex_coe not_isReal_iff_isComplex card_filter_mk_eq Fintype.card.eq_1 Finset.card_eq_sum_ones Finset.sum_fiberwise Finset.sum_congr Finset.sum_const mul_one Finset.mul_sum
card_eq_nrRealPlaces_add_nrComplexPlaces 📖	mathematical	—	Fintype.card NumberField.InfinitePlace NumberField.InfinitePlace.fintype nrRealPlaces nrComplexPlaces	—	Fintype.card_of_subtype isReal_or_isComplex Fintype.card_subtype_or_disjoint disjoint_isReal_isComplex
card_filter_mk_eq 📖	mathematical	—	Finset.card RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring Finset.filter NumberField.InfinitePlace Finset.univ NumberField.Embeddings.instFintypeRingHom Complex.instField Complex.instCharZero mult	—	Complex.instCharZero mk_embedding mk_eq_iff NumberField.ComplexEmbedding.conjugate.eq_1 Function.Involutive.eq_iff InvolutiveStar.star_involutive Finset.filter_or Finset.filter_eq' NumberField.ComplexEmbedding.isReal_iff isReal_iff Finset.union_idempotent Finset.card_singleton Finset.card_pair
card_real_embeddings 📖	mathematical	—	Fintype.card RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring NumberField.ComplexEmbedding.IsReal Subtype.fintype NumberField.Embeddings.instFintypeRingHom Complex.instField Complex.instCharZero nrRealPlaces	—	Fintype.card_congr Complex.instCharZero
coe_apply 📖	mathematical	—	DFunLike.coe NumberField.InfinitePlace Real instFunLikeReal AbsoluteValue DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder AbsoluteValue.funLike RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial	—	—
conjugate_embedding_eq_of_isReal 📖	mathematical	IsReal	NumberField.ComplexEmbedding.conjugate embedding	—	NumberField.ComplexEmbedding.isReal_iff isReal_iff
conjugate_embedding_injective 📖	mathematical	—	NumberField.InfinitePlace RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring NumberField.ComplexEmbedding.conjugate embedding	—	star_injective embedding_injective
denseRange_algebraMap_pi 📖	mathematical	—	DenseRange Pi.topologicalSpace NumberField.InfinitePlace WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField DFunLike.coe CommSemiring.toSemiring Semifield.toCommSemiring Pi.semiring WithAbs.instSemiring RingHom.instFunLike algebraMap Pi.algebra WithAbs.instAlgebra_right Algebra.id	—	Complex.instNontrivial Metric.denseRange_iff tendsto_pi_nhds Fintype.sum_pi_single map_sum RingHomClass.toAddMonoidHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Finset.sum_congr map_mul NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass tendsto_finset_sum IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Pi.single_apply map_inv₀ instMonoidWithZeroHomClassReal IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass inv_pow one_div RingHomClass.toMonoidWithZeroHomClass map_add AddMonoidHomClass.toAddHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass map_pow RingEquiv.symm_apply_apply one_mul Filter.Tendsto.mul_const IsTopologicalSemiring.toContinuousMul WithAbs.tendsto_one_div_one_add_pow_nhds_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE pos_iff Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing map_zero MonoidWithZeroHomClass.toZeroHomClass MulZeroClass.zero_mul tendsto_zero_iff_norm_tendsto_zero AbsoluteValue.tendsto_div_one_add_pow_nhds_zero Real.instArchimedean instOrderTopologyReal Metric.tendsto_atTop le_rfl dist_comm AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquiv Finite.of_fintype isNontrivial Iff.not eq_iff_isEquiv
disjoint_isReal_isComplex 📖	mathematical	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice setOf IsReal IsComplex	—	Set.disjoint_iff not_isReal_iff_isComplex
embedding_inj 📖	mathematical	—	embedding	—	embedding_injective
embedding_injective 📖	mathematical	—	NumberField.InfinitePlace RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring embedding	—	mk_embedding
embedding_mk_eq 📖	mathematical	—	embedding NumberField.ComplexEmbedding.conjugate	—	mk_eq_iff mk_embedding
embedding_mk_eq_of_isReal 📖	mathematical	NumberField.ComplexEmbedding.IsReal	embedding	—	embedding_mk_eq NumberField.ComplexEmbedding.isReal_iff
embedding_of_isReal_apply 📖	mathematical	IsReal	Complex.ofReal DFunLike.coe RingHom Real Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring RingHom.instFunLike embedding_of_isReal Complex Complex.instSemiring embedding	—	NumberField.ComplexEmbedding.IsReal.coe_embedding_apply isReal_iff
eq_iff_eq 📖	mathematical	—	DFunLike.coe NumberField.InfinitePlace Real instFunLikeReal Norm.norm Complex Complex.instNorm RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring RingHom.instFunLike	—	Complex.instNontrivial
eq_iff_isEquiv 📖	mathematical	—	AbsoluteValue.IsEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real Real.semiring Real.partialOrder AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial	—	Complex.instNontrivial AbsoluteValue.IsEquiv.rfl AbsoluteValue.isEquiv_iff_exists_rpow_eq ext eq_one_of_rpow_eq Real.rpow_one
eq_of_embedding_eq_conjugate 📖	—	embedding NumberField.ComplexEmbedding.conjugate	—	—	mk_embedding mk_conjugate_eq
eq_one_of_rpow_eq 📖	mathematical	Real Pi.instPow Real.instPow DFunLike.coe NumberField.InfinitePlace instFunLikeReal	Real.instOne	—	NoMaxOrder.exists_gt Nat.instNoMaxOrder RCLike.charZero_rclike Real.rpow_one map_natCast
ext 📖	—	DFunLike.coe NumberField.InfinitePlace Real instFunLikeReal	—	—	Complex.instNontrivial AbsoluteValue.ext
ext_iff 📖	mathematical	—	DFunLike.coe NumberField.InfinitePlace Real instFunLikeReal	—	ext
instMonoidWithZeroHomClassReal 📖	mathematical	—	MonoidWithZeroHomClass NumberField.InfinitePlace Real NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring instFunLikeReal	—	AbsoluteValue.map_mul Complex.instNontrivial AbsoluteValue.map_one Real.instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing AbsoluteValue.map_zero
instNonnegHomClassReal 📖	mathematical	—	NonnegHomClass NumberField.InfinitePlace Real Real.instZero Real.instLE instFunLikeReal	—	AbsoluteValue.nonneg Complex.instNontrivial
isComplex_iff 📖	mathematical	—	IsComplex NumberField.ComplexEmbedding.IsReal embedding	—	Mathlib.Tactic.Contrapose.contrapose₄ mk_eq_iff mk_embedding NumberField.ComplexEmbedding.isReal_conjugate_iff
isComplex_mk_iff 📖	mathematical	—	IsComplex NumberField.ComplexEmbedding.IsReal	—	not_isReal_iff_isComplex Iff.not isReal_mk_iff
isInfinitePlace 📖	mathematical	—	NumberField.IsInfinitePlace AbsoluteValue Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial	—	Subtype.prop Complex.instNontrivial
isNontrivial 📖	mathematical	—	AbsoluteValue.IsNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real Real.semiring Real.partialOrder AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial	—	Complex.instNontrivial NoMaxOrder.exists_gt Nat.instNoMaxOrder pos_iff LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike map_natCast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
isReal_iff 📖	mathematical	—	IsReal NumberField.ComplexEmbedding.IsReal embedding	—	embedding_mk_eq_of_isReal mk_embedding
isReal_mk_iff 📖	mathematical	—	IsReal NumberField.ComplexEmbedding.IsReal	—	isReal_of_mk_isReal
isReal_of_mk_isReal 📖	mathematical	IsReal	NumberField.ComplexEmbedding.IsReal	—	Mathlib.Tactic.Contrapose.contrapose₁ not_isReal_iff_isComplex
isReal_or_isComplex 📖	mathematical	—	IsReal IsComplex	—	not_isReal_iff_isComplex em
le_iff_le 📖	mathematical	—	Real Real.instLE DFunLike.coe NumberField.InfinitePlace instFunLikeReal Norm.norm Complex Complex.instNorm RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring RingHom.instFunLike	—	Complex.instNontrivial
map_intCast 📖	mathematical	—	DFunLike.coe NumberField.InfinitePlace Real instFunLikeReal AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Norm.norm NormedRing.toNorm NormedCommRing.toNormedRing Int.instNormedCommRing	—	Complex.instNontrivial map_intCast RingHom.instRingHomClass Complex.norm_intCast
map_natCast 📖	mathematical	—	DFunLike.coe NumberField.InfinitePlace Real instFunLikeReal AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Real.instNatCast	—	Complex.instNontrivial map_natCast RingHom.instRingHomClass RCLike.norm_natCast
map_ratCast 📖	mathematical	—	DFunLike.coe NumberField.InfinitePlace Real instFunLikeReal DivisionRing.toRatCast Field.toDivisionRing Norm.norm NormedField.toNorm Rat.instNormedField	—	Complex.instNontrivial map_ratCast RingHom.instRingHomClass Complex.norm_ratCast
mkComplex_coe 📖	mathematical	—	NumberField.InfinitePlace IsComplex mkComplex RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring NumberField.ComplexEmbedding.IsReal	—	—
mkReal_coe 📖	mathematical	—	NumberField.InfinitePlace IsReal DFunLike.coe Equiv RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring NumberField.ComplexEmbedding.IsReal EquivLike.toFunLike Equiv.instEquivLike mkReal	—	—
mk_conjugate_eq 📖	mathematical	—	NumberField.ComplexEmbedding.conjugate	—	DFunLike.ext apply NumberField.ComplexEmbedding.conjugate_coe_eq Complex.norm_conj
mk_embedding 📖	mathematical	—	embedding	—	Complex.instNontrivial
mk_eq_iff 📖	mathematical	—	NumberField.ComplexEmbedding.conjugate	—	Function.Injective.hasLeftInverse Nontrivial.to_nonempty IsLocalRing.toNontrivial Field.instIsLocalRing RingHom.injective DivisionRing.isSimpleRing Complex.instNontrivial SubringClass.toSubsemiringClass Subring.instSubringClass LipschitzWith.of_dist_le_mul NNReal.coe_one one_mul NormedField.dist_eq map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass le_of_eq SubringClass.addSubgroupClass RingEquiv.ofLeftInverse_apply RingEquiv.apply_symm_apply Complex.uniformContinuous_ringHom_eq_id_or_conj LipschitzWith.uniformContinuous RingHom.ext mk_conjugate_eq
mult_coe_ne_zero 📖	—	—	—	—	Nat.cast_ne_zero RCLike.charZero_rclike mult_ne_zero
mult_isComplex 📖	mathematical	—	mult NumberField.InfinitePlace IsComplex	—	mult.eq_1 not_isReal_iff_isComplex Subtype.prop
mult_isReal 📖	mathematical	—	mult NumberField.InfinitePlace IsReal	—	mult.eq_1 Subtype.prop
mult_ne_zero 📖	—	—	—	—	ne_of_gt mult_pos
mult_pos 📖	mathematical	—	mult	—	mult.eq_1 Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instCharZero Mathlib.Meta.NormNum.isNat_ofNat
ne_of_isReal_isComplex 📖	—	IsReal IsComplex	—	—	not_isReal_iff_isComplex
norm_embedding_eq 📖	mathematical	—	Norm.norm Complex Complex.instNorm DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring RingHom.instFunLike embedding NumberField.InfinitePlace Real instFunLikeReal	—	mk_embedding
norm_embedding_of_isReal 📖	mathematical	IsReal	Norm.norm Real Real.norm DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring RingHom.instFunLike embedding_of_isReal NumberField.InfinitePlace instFunLikeReal	—	norm_embedding_eq embedding_of_isReal_apply Complex.norm_real
not_isComplex_iff_isReal 📖	mathematical	—	IsComplex IsReal	—	isComplex_iff isReal_iff
not_isReal_iff_isComplex 📖	mathematical	—	IsReal IsComplex	—	isComplex_iff isReal_iff
not_isReal_of_mk_isComplex 📖	mathematical	IsComplex	NumberField.ComplexEmbedding.IsReal	—	isComplex_mk_iff
nrComplexPlaces_eq_zero_of_finrank_eq_one 📖	mathematical	Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	nrComplexPlaces	—	NumberField.to_charZero Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Mathlib.Tactic.Linarith.natCast_nonneg Nat.cast_zero Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Linarith.lt_of_lt_of_eq sub_eq_zero_of_eq Nat.cast_one Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Meta.NormNum.isNat_lt_true Int.instCharZero Nat.cast_add Nat.cast_mul card_add_two_mul_card_eq_rank
nrRealPlaces_eq_one_of_finrank_eq_one 📖	mathematical	Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	nrRealPlaces	—	NumberField.to_charZero card_add_two_mul_card_eq_rank add_zero MulZeroClass.mul_zero nrComplexPlaces_eq_zero_of_finrank_eq_one
nrRealPlaces_pos_of_odd_finrank 📖	mathematical	Odd Nat.instSemiring Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	nrRealPlaces	—	NumberField.to_charZero Nat.not_odd_iff_even card_add_two_mul_card_eq_rank zero_add even_two_mul
one_le_mult 📖	mathematical	—	Real Real.instLE Real.instOne Real.instNatCast mult	—	Nat.cast_one Nat.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike mult_pos
one_le_of_lt_one 📖	mathematical	Real Real.instLT DFunLike.coe NumberField.InfinitePlace instFunLikeReal NumberField.RingOfIntegers.val Real.instOne	Real.instLE	—	NumberField.to_charZero Algebra.coe_norm_int Int.cast_one Int.cast_abs Rat.instIsStrictOrderedRing Rat.cast_intCast Int.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Int.one_le_abs Algebra.norm_ne_zero_iff Int.instIsDomain NumberField.RingOfIntegers.instIsDomain NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt Mathlib.Tactic.Contrapose.contrapose₁ prod_eq_abs_norm Finset.prod_const_one Finset.prod_lt_prod_of_nonempty IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instNontrivial pow_pos pos_iff AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass Iff.not Subalgebra.coe_eq_zero pow_lt_one₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing NonnegHomClass.apply_nonneg instNonnegHomClassReal mult.eq_1 Mathlib.Meta.NormNum.isNat_eq_false Nat.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Finset.univ_nonempty NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed
pos_iff 📖	mathematical	—	Real Real.instLT Real.instZero DFunLike.coe NumberField.InfinitePlace instFunLikeReal	—	AbsoluteValue.pos_iff Complex.instNontrivial
prod_eq_abs_norm 📖	mathematical	—	Finset.prod NumberField.InfinitePlace Real Real.instCommMonoid Finset.univ NumberField.InfinitePlace.fintype Monoid.toNatPow Real.instMonoid DFunLike.coe instFunLikeReal mult Real.instRatCast abs Rat.instLattice Rat.addGroup MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring Rat.commRing MonoidHom.instFunLike Algebra.norm DivisionRing.toRatAlgebra NumberField.to_charZero	—	NumberField.to_charZero Complex.instCharZero instIsDomain NumberField.to_finiteDimensional norm_prod NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Fintype.prod_equiv Finset.prod_fiberwise Finset.mem_filter apply Finset.prod_congr Finset.prod_const card_filter_mk_eq eq_ratCast RingHom.instRingHomClass Rat.cast_abs Real.instIsStrictOrderedRing Real.norm_eq_abs Complex.norm_real Complex.ofReal_ratCast Algebra.norm_eq_prod_embeddings Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite Rat.nontrivial PerfectField.ofCharZero Rat.instCharZero Complex.isAlgClosed
prod_eq_prod_mul_prod 📖	mathematical	—	Finset.prod NumberField.InfinitePlace Finset.univ NumberField.InfinitePlace.fintype MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid IsReal Subtype.fintype IsComplex	—	not_isReal_iff_isComplex Equiv.prod_comp Finset.prod_congr Fintype.prod_subtype_mul_prod_subtype
sum_eq_sum_add_sum 📖	mathematical	—	Finset.sum NumberField.InfinitePlace Finset.univ NumberField.InfinitePlace.fintype AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid IsReal Subtype.fintype IsComplex	—	not_isReal_iff_isComplex Equiv.sum_comp Finset.sum_congr Fintype.sum_subtype_add_sum_subtype
sum_mult_eq 📖	mathematical	—	Finset.sum NumberField.InfinitePlace Nat.instAddCommMonoid Finset.univ NumberField.InfinitePlace.fintype mult Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	NumberField.to_charZero Complex.instCharZero NumberField.Embeddings.card Complex.isAlgClosed Fintype.card.eq_1 Finset.card_eq_sum_ones Finset.sum_fiberwise Finset.sum_congr Finset.sum_const smul_eq_mul mul_one card_filter_mk_eq

NumberField.InfinitePlace.ComplexEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjugate_sign 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign NumberField.Embeddings.instFintypeRingHom Complex.instField Complex.instCharZero Function.Involutive.toPerm NumberField.ComplexEmbedding.conjugate NumberField.ComplexEmbedding.involutive_conjugate Int.instUnitsPow Nat.instCommSemiring AddCommMonoid.toNatModule Additive Additive.addCommMonoid CommGroup.toCommMonoid Units.instCommGroupUnits Int.instCommMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Units.instOne NumberField.InfinitePlace.nrComplexPlaces	—	Complex.instCharZero NumberField.ComplexEmbedding.involutive_conjugate Equiv.Perm.sign_of_pow_two_eq_one Equiv.ext Function.Involutive.toPerm_involutive NumberField.to_charZero NumberField.Embeddings.card Complex.isAlgClosed NumberField.InfinitePlace.card_add_two_mul_card_eq_rank NumberField.InfinitePlace.card_real_embeddings Fintype.card.eq_1 Nat.instAtLeastTwoHAddOfNat zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid

NumberField.InfinitePlace.IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nrRealPlaces_eq_zero_of_two_lt 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	NumberField.InfinitePlace.nrRealPlaces	—	Fintype.card_eq_zero_iff IsPrimitiveRoot.map_of_injective MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.injective DivisionRing.isSimpleRing Complex.instNontrivial Complex.conj_eq_iff_im NumberField.ComplexEmbedding.conjugate_coe_eq NumberField.InfinitePlace.isReal_iff Complex.norm_eq_one_of_pow_eq_one IsPrimitiveRoot.pow_eq_one abs_eq_abs abs_one Real.instIsOrderedRing Complex.abs_re_eq_norm IsPrimitiveRoot.ne_one Complex.ext IsPrimitiveRoot.eq_orderOf neg_zero orderOf_neg_one ringChar.eq_zero Complex.instCharZero Nat.instCharZero Nat.instAtLeastTwoHAddOfNat

NumberField.InfinitePlace.NumberField.InfinitePlace

Definitions

Name	Category	Theorems
fintype 📖	CompOp	96 math math: NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', NumberField.mixedEmbedding.fundamentalDomain_integerLattice, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, NumberField.InfinitePlace.sum_mult_eq, NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, NumberField.mixedEmbedding.norm_le_convexBodySumFun, NumberField.Units.regOfFamily_eq_det, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, NumberField.InfinitePlace.card_mono, NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume, NumberField.prod_abs_eq_one, NumberField.mixedEmbedding.convexBodyLT_volume, NumberField.mixedEmbedding.convexBodySumFun_apply', NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, NumberField.Units.instZLattice_unitLattice, NumberField.mulHeight_eq, NumberField.Units.regulator_eq_det, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, NumberField.Units.finrank_mul_regOfFamily_eq_det, NumberField.mixedEmbedding.convexBodySumFun_apply, NumberField.InfinitePlace.card_eq_card_isUnramifiedIn, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, NumberField.mixedEmbedding.realSpace.volume_eq_zero, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.mixedEmbedding.volume_preserving_negAt, NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow, NumberField.InfinitePlace.card_isUnramified, NumberField.mixedEmbedding.adjust_f, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, NumberField.Units.regOfFamily_of_isMaxRank, NumberField.IsCMField.card_infinitePlace_eq_card_infinitePlace, NumberField.InfinitePlace.card_isUnramified_compl, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, NumberField.mixedEmbedding.det_matrixToStdBasis, NumberField.mixedEmbedding.covolume_integerLattice, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, NumberField.Units.abs_det_eq_abs_det, NumberField.mixedEmbedding.volume_negAt_plusPart, NumberField.mixedEmbedding.convexBodyLT'_volume, NumberField.InfinitePlace.sum_eq_sum_add_sum, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, NumberField.mixedEmbedding.volume_eq_zero, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, IsUnramifiedAtInfinitePlaces.card_infinitePlace, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, NumberField.InfinitePlace.prod_eq_prod_mul_prod, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply, NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, NumberField.mixedEmbedding.fundamentalCone.sum_eq_zero_of_mem_span_completeFamily, NumberField.mixedEmbedding.fundamentalCone.compactSet_ae, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, NumberField.prod_archAbsVal_eq, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, NumberField.Units.finrank_mul_regulator_eq_det, NumberField.InfinitePlace.prod_eq_abs_norm, NumberField.mulHeight₁_eq, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, NumberField.Units.sum_mult_mul_log, NumberField.mixedEmbedding.convexBodySum_volume, NumberField.Units.regulator_eq_det', NumberField.mixedEmbedding.integral_comp_polarCoord_symm, NumberField.Units.basisOfIsMaxRank_fundSystem, NumberField.Units.regOfFamily_eq_det', NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart, NumberField.mixedEmbedding.convexBodySum_mem, NumberField.mixedEmbedding.norm_apply, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm

Rat

Definitions

Name	Category	Theorems
infinitePlace 📖	CompOp	1 math math: isReal_infinitePlace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infinitePlace_apply 📖	mathematical	—	DFunLike.coe NumberField.InfinitePlace instField Real NumberField.InfinitePlace.instFunLikeReal Real.instRatCast abs instLattice addGroup	—	Complex.instNontrivial NumberField.InfinitePlace.coe_apply eq_ratCast RingHom.instRingHomClass Complex.norm_ratCast cast_abs Real.instIsStrictOrderedRing
instSubsingletonInfinitePlace 📖	mathematical	—	NumberField.InfinitePlace instField	—	NumberField.InfinitePlace.ext infinitePlace_apply cast_abs Real.instIsStrictOrderedRing
isReal_infinitePlace 📖	mathematical	—	NumberField.InfinitePlace.IsReal instField infinitePlace	—	Complex.instCharZero RingHom.ext eq_ratCast RingHom.instRingHomClass

---

← Back to Index