InfinitePlace

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

Statistics

Metric	Count
Definitions InfinitePlace, extensionEmbedding, extensionEmbeddingOfIsReal, instAlgebra, instNormedField, isometryEquivComplexOfIsComplex, isometryEquivRealOfIsReal, ringEquivComplexOfIsComplex, ringEquivRealOfIsReal	9
Theorems norm_infinitePlace_completion, ratCast_equiv, algebraMap_coe, bijective_extensionEmbeddingOfIsReal, bijective_extensionEmbedding_of_isComplex, extensionEmbeddingOfIsReal_apply, extensionEmbeddingOfIsReal_coe, extensionEmbedding_coe, instIsTopologicalRing, isClosed_image_extensionEmbedding, isClosed_image_extensionEmbeddingOfIsReal, isometry_extensionEmbedding, isometry_extensionEmbeddingOfIsReal, liesOver_conjugate_extensionEmbedding, liesOver_extensionEmbedding, locallyCompactSpace, norm_coe, subfield_ne_real_of_isComplex, surjective_extensionEmbeddingOfIsReal, surjective_extensionEmbedding_of_isComplex, embedding_liesOver_of_isReal, extensionEmbedding_liesOver_of_isReal, isometry_algebraMap, isometry_embedding, isometry_embedding_of_isReal	25
Total	34

NumberField

Definitions

Name	Category	Theorems
InfinitePlace 📖	CompOp	386 math math: InfinitePlace.mult_isComplex, mixedEmbedding.integral_comp_polarSpaceCoord_symm, mixedEmbedding.fundamentalCone.expMapBasis_apply', mixedEmbedding.fundamentalDomain_integerLattice, InfinitePlace.mk_mem_ramifiedPlacesOver, mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, mixedEmbedding.logMap_one, mixedEmbedding.lintegral_comp_polarCoord_symm, InfinitePlace.norm_embedding_of_isReal, mixedEmbedding.fundamentalCone.interior_paramSet, mixedEmbedding.measurable_polarCoordReal_symm, mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet_mixedEmbedding, 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, isInfinitePlace_iff, InfinitePlace.isUnramified_iff_card_stabilizer_eq_one, IsCMField.equivInfinitePlace_symm_apply, instNonemptyInfinitePlaceOfRingHomComplex, mixedEmbedding.normAtAllPlaces_apply, mixedEmbedding.norm_eq_zero_iff', 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, mixedEmbedding.measurableSet_plusPart, 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, Units.dirichletUnitTheorem.logEmbedding_component_le, 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.ramifiedPlacesOver_ncard, 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, mixedEmbedding.negAt_apply_isReal_and_notMem, Units.dirichletUnitTheorem.unitLattice_span_eq_top, mixedEmbedding.covolume_idealLattice, mixedEmbedding.fundamentalCone.expMap_basis_of_eq, mixedEmbedding.volume_preserving_negAt, mixedEmbedding.normAtPlace_add_le, totalWeight_eq_sum_mult, 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.exists_ne_zero_mem_ringOfIntegers_lt', mixedEmbedding.convexBodySumFun_continuous, InfinitePlace.card_isUnramified_compl, mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, mixedEmbedding.logMap_eq_logEmbedding, mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, mixedEmbedding.logMap_apply_of_norm_eq_one, mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, mixedEmbedding.fundamentalCone.hasFDerivAt_expMap, logHeight₁_eq, Units.dirichletUnitTheorem.mult_log_place_eq_zero, mixedEmbedding.norm_nonneg, mixedEmbedding.mixedEmbedding_apply_isReal, Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, 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.exists_ne_zero_mem_ideal_lt, 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, mixedEmbedding.negAt_apply_isReal_and_mem, Units.abs_det_eq_abs_det, mixedEmbedding.polarSpaceCoord_target', mixedEmbedding.exists_primitive_element_lt_of_isReal, mixedEmbedding.volume_negAt_plusPart, 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.exists_ne_zero_mem_ringOfIntegers_lt, InfinitePlace.bijOn_sumElim_conjugate, mixedEmbedding.indexEquiv_apply_isReal, mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, 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.exists_ne_zero_mem_ideal_lt', mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, mixedEmbedding.normAtPlace_apply_of_isComplex, mixedEmbedding_injective, InfinitePlace.comap_smul, InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two, InfinitePlace.union_ramifiedPlacesOver_unramifiedPlacesOver, mixedEmbedding.forall_normAtPlace_eq_zero_iff, mixedEmbedding.convexBodyLT_convex, mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, mixedEmbedding.fundamentalCone.logMap_expMap, 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.logMap_apply_of_norm_one, 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, InfinitePlace.mk_mem_unramifiedPlacesOver, 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, mixedEmbedding.norm_eq_of_normAtPlace_eq, InfinitePlace.prod_eq_prod_mul_prod, InfinitePlace.mkComplex_coe, mixedEmbedding.fundamentalCone.expMapBasis_apply, Units.unitLattice_rank, InfinitePlace.disjoint_ramifiedPlacesOver_unramifiedPlacesOver, InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces, mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_snd, mixedEmbedding.norm_real, mixedEmbedding.volume_fundamentalDomain_latticeBasis, Units.logEmbeddingEquiv_apply, mixedEmbedding.polarSpaceCoord_source, mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, InfiniteAdeleRing.norm_def, InfinitePlace.mem_orbit_iff, mixedEmbedding.indexEquiv_apply_isComplex_snd, InfinitePlace.eq_iff_eq, mixedEmbedding.polarCoord_target_eq_polarCoordReal_target, mixedEmbedding.fundamentalCone.sum_eq_zero_of_mem_span_completeFamily, InfinitePlace.map_intCast, mixedEmbedding.fundamentalCone.compactSet_ae, mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, mixedEmbedding.euclidean.finrank, mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, mixedEmbedding.measurableSet_negAt_plusPart, 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.exists_normAtPlace_ne_zero_iff, mixedEmbedding.mixedEmbedding_apply_isComplex, InfinitePlace.one_le_of_lt_one, 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.volume_eq_two_pi_pow_mul_integral, 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, InfinitePlace.unramifiedPlacesOver_ncard, 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, sum_archAbsVal_eq, mixedEmbedding.fundamentalCone.injective_expMap, mixedEmbedding.fundamentalCone.expMap_basis_of_ne, mixedEmbedding.disjoint_negAt_plusPart, mixedEmbedding.logMap_mul, mixedEmbedding.volume_fundamentalDomain_stdBasis, mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart, mixedEmbedding.convexBodySum_mem, mixedEmbedding.fundamentalCone.expMapBasis_nonneg, mixedEmbedding.convexBodyLT'_convex, mixedEmbedding.mem_rat_span_latticeBasis, InfinitePlace.unramifedPlacesOver_ncard_add_eq_finrank, 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

NumberField.InfinitePlace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isometry_embedding 📖	mathematical	—	Isometry 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 EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace WithAbs.normedField DFunLike.coe WithAbs.instSemiring RingHom.instFunLike RingHom.comp embedding RingEquiv.toRingHom WithAbs.equiv	—	AddMonoidHomClass.isometry_of_norm Complex.instNontrivial RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass norm_embedding_eq
isometry_embedding_of_isReal 📖	mathematical	IsReal	Isometry 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 EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace WithAbs.normedField Real.metricSpace DFunLike.coe WithAbs.instSemiring RingHom.instFunLike RingHom.comp embedding_of_isReal RingEquiv.toRingHom WithAbs.equiv	—	AddMonoidHomClass.isometry_of_norm Complex.instNontrivial RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass norm_embedding_of_isReal

NumberField.InfinitePlace.Completion

Definitions

Name	Category	Theorems
extensionEmbedding 📖	CompOp	10 math math: surjective_extensionEmbedding_of_isComplex, isometry_extensionEmbedding, isClosed_image_extensionEmbedding, extensionEmbedding_coe, extensionEmbeddingOfIsReal_apply, bijective_extensionEmbedding_of_isComplex, NumberField.InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal, liesOver_extensionEmbedding, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, liesOver_conjugate_extensionEmbedding
extensionEmbeddingOfIsReal 📖	CompOp	7 math math: isometry_extensionEmbeddingOfIsReal, extensionEmbeddingOfIsReal_coe, isClosed_image_extensionEmbeddingOfIsReal, extensionEmbeddingOfIsReal_apply, bijective_extensionEmbeddingOfIsReal, surjective_extensionEmbeddingOfIsReal, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply
instAlgebra 📖	CompOp	—
instNormedField 📖	CompOp	18 math math: isometry_extensionEmbeddingOfIsReal, surjective_extensionEmbedding_of_isComplex, isometry_extensionEmbedding, isClosed_image_extensionEmbedding, extensionEmbeddingOfIsReal_coe, isClosed_image_extensionEmbeddingOfIsReal, extensionEmbedding_coe, extensionEmbeddingOfIsReal_apply, bijective_extensionEmbeddingOfIsReal, bijective_extensionEmbedding_of_isComplex, algebraMap_coe, NumberField.InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal, surjective_extensionEmbeddingOfIsReal, liesOver_extensionEmbedding, WithAbs.ratCast_equiv, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, Rat.norm_infinitePlace_completion, liesOver_conjugate_extensionEmbedding
isometryEquivComplexOfIsComplex 📖	CompOp	—
isometryEquivRealOfIsReal 📖	CompOp	—
ringEquivComplexOfIsComplex 📖	CompOp	—
ringEquivRealOfIsReal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_coe 📖	mathematical	—	DFunLike.coe RingHom NumberField.InfinitePlace.Completion Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField instNormedField DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap UniformSpace.Completion.coe' WithAbs Real Real.semiring Real.partialOrder AbsoluteValue Complex Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField WithAbs.instCommSemiring WithAbs.instSemiring WithAbs.algebraLeft WithAbs.instAlgebra	—	Complex.instNontrivial WithAbs.instUniformContinuousConstSMulReal IsScalarTower.algebraMap_apply WithAbs.instIsScalarTower UniformSpace.Completion.algebraMap_def
bijective_extensionEmbeddingOfIsReal 📖	mathematical	NumberField.InfinitePlace.IsReal	Function.Bijective NumberField.InfinitePlace.Completion Real DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal	—	RingHom.injective DivisionRing.isSimpleRing Real.instNontrivial surjective_extensionEmbeddingOfIsReal
bijective_extensionEmbedding_of_isComplex 📖	mathematical	NumberField.InfinitePlace.IsComplex	Function.Bijective NumberField.InfinitePlace.Completion Complex DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Complex.instSemiring RingHom.instFunLike extensionEmbedding	—	RingHom.injective DivisionRing.isSimpleRing Complex.instNontrivial surjective_extensionEmbedding_of_isComplex
extensionEmbeddingOfIsReal_apply 📖	mathematical	NumberField.InfinitePlace.IsReal	Complex.ofReal DFunLike.coe RingHom NumberField.InfinitePlace.Completion Real Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal Complex Complex.instSemiring extensionEmbedding	—	UniformSpace.Completion.induction_on Complex.instNontrivial isClosed_eq Complex.instT2Space Continuous.comp' Complex.continuous_ofReal UniformSpace.Completion.continuous_extension Real.instCompleteSpace Complex.instCompleteSpace extensionEmbeddingOfIsReal_coe NumberField.InfinitePlace.embedding_of_isReal_apply extensionEmbedding_coe
extensionEmbeddingOfIsReal_coe 📖	mathematical	NumberField.InfinitePlace.IsReal	DFunLike.coe RingHom NumberField.InfinitePlace.Completion Real Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal UniformSpace.Completion.coe' WithAbs Real.partialOrder AbsoluteValue Complex Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField NumberField.InfinitePlace.embedding_of_isReal RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring WithAbs.instSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike WithAbs.equiv	—	Complex.instNontrivial Isometry.extensionHom_coe IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup instIsUniformAddGroupReal instIsTopologicalRingReal Real.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding_of_isReal
extensionEmbedding_coe 📖	mathematical	—	DFunLike.coe RingHom NumberField.InfinitePlace.Completion Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Complex.instSemiring RingHom.instFunLike extensionEmbedding UniformSpace.Completion.coe' WithAbs Real Real.semiring Real.partialOrder AbsoluteValue NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField NumberField.InfinitePlace.embedding RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring WithAbs.instSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike WithAbs.equiv	—	Complex.instNontrivial Isometry.extensionHom_coe IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup Complex.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding
instIsTopologicalRing 📖	mathematical	—	IsTopologicalRing NumberField.InfinitePlace.Completion UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace 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 PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing UniformSpace.Completion.instNormedCommRing	—	UniformSpace.Completion.topologicalRing Complex.instNontrivial
isClosed_image_extensionEmbedding 📖	mathematical	—	IsClosed Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set.range NumberField.InfinitePlace.Completion DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Complex.instSemiring RingHom.instFunLike extensionEmbedding	—	Topology.IsClosedEmbedding.isClosed_range Complex.instNontrivial Isometry.isClosedEmbedding UniformSpace.Completion.completeSpace Isometry.completion_extension Complex.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding
isClosed_image_extensionEmbeddingOfIsReal 📖	mathematical	NumberField.InfinitePlace.IsReal	IsClosed Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.range NumberField.InfinitePlace.Completion DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal	—	Topology.IsClosedEmbedding.isClosed_range Complex.instNontrivial Isometry.isClosedEmbedding UniformSpace.Completion.completeSpace Isometry.completion_extension Real.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding_of_isReal
isometry_extensionEmbedding 📖	mathematical	—	Isometry NumberField.InfinitePlace.Completion Complex EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace UniformSpace.Completion.instMetricSpace WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AbsoluteValue RingHom Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField NormedField.toMetricSpace DFunLike.coe NormedField.toField instNormedField RingHom.instFunLike extensionEmbedding	—	Isometry.completion_extension Complex.instNontrivial Complex.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding
isometry_extensionEmbeddingOfIsReal 📖	mathematical	NumberField.InfinitePlace.IsReal	Isometry NumberField.InfinitePlace.Completion Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace UniformSpace.Completion.instMetricSpace WithAbs 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField Real.metricSpace DFunLike.coe NormedField.toField instNormedField RingHom.instFunLike extensionEmbeddingOfIsReal	—	Isometry.completion_extension Complex.instNontrivial Real.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NumberField.InfinitePlace.isometry_embedding_of_isReal
liesOver_conjugate_extensionEmbedding 📖	mathematical	—	NumberField.ComplexEmbedding.LiesOver NumberField.InfinitePlace.Completion NormedField.toField instNormedField NumberField.ComplexEmbedding.conjugate extensionEmbedding	—	Complex.instNontrivial RingHom.ext UniformSpace.Completion.induction_on isClosed_eq Complex.instT2Space Continuous.comp Complex.continuous_conj UniformSpace.Completion.continuous_extension Complex.instCompleteSpace continuous_algebraMap algebraMap_coe extensionEmbedding_coe NumberField.ComplexEmbedding.LiesOver.over
liesOver_extensionEmbedding 📖	mathematical	—	NumberField.ComplexEmbedding.LiesOver NumberField.InfinitePlace.Completion NormedField.toField instNormedField extensionEmbedding	—	Complex.instNontrivial RingHom.ext UniformSpace.Completion.induction_on isClosed_eq Complex.instT2Space Continuous.comp UniformSpace.Completion.continuous_extension Complex.instCompleteSpace continuous_algebraMap algebraMap_coe extensionEmbedding_coe NumberField.ComplexEmbedding.LiesOver.over
locallyCompactSpace 📖	mathematical	—	LocallyCompactSpace NumberField.InfinitePlace.Completion UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace 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 PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField	—	AbsoluteValue.Completion.locallyCompactSpace Complex.instNontrivial Complex.instCompleteSpace locallyCompact_of_proper Complex.instProperSpace NumberField.InfinitePlace.isometry_embedding
norm_coe 📖	mathematical	—	Norm.norm UniformSpace.Completion 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 PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField UniformSpace.Completion.instNorm NormedField.toNorm UniformSpace.Completion.coe' DFunLike.coe NumberField.InfinitePlace NumberField.InfinitePlace.instFunLikeReal RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring WithAbs.instSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike WithAbs.equiv	—	Complex.instNontrivial UniformSpace.Completion.norm_coe
subfield_ne_real_of_isComplex 📖	—	NumberField.InfinitePlace.IsComplex	—	—	Mathlib.Tactic.Contrapose.contrapose₃ RingHom.ext Complex.instNontrivial RingHom.mem_fieldRange_self RingEquiv.apply_symm_apply WithAbs.equiv_symm_apply extensionEmbedding_coe Complex.conj_ofReal
surjective_extensionEmbeddingOfIsReal 📖	mathematical	NumberField.InfinitePlace.IsReal	NumberField.InfinitePlace.Completion Real DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Real.semiring RingHom.instFunLike extensionEmbeddingOfIsReal	—	RingHom.fieldRange_eq_top_iff Real.subfield_eq_of_closed isClosed_image_extensionEmbeddingOfIsReal
surjective_extensionEmbedding_of_isComplex 📖	mathematical	NumberField.InfinitePlace.IsComplex	NumberField.InfinitePlace.Completion Complex DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instNormedField Complex.instSemiring RingHom.instFunLike extensionEmbedding	—	RingHom.fieldRange_eq_top_iff Complex.subfield_eq_of_closed isClosed_image_extensionEmbedding subfield_ne_real_of_isComplex

NumberField.InfinitePlace.Completion.Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_infinitePlace_completion 📖	mathematical	—	Norm.norm NumberField.InfinitePlace.Completion Rat.instField UniformSpace.Completion.instNorm 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 PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField NormedField.toNorm DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NumberField.InfinitePlace.Completion.instNormedField Real.instRatCast abs Rat.instLattice Rat.addGroup	—	Complex.instNontrivial RingEquiv.apply_symm_apply NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv NumberField.InfinitePlace.Completion.norm_coe Rat.infinitePlace_apply

NumberField.InfinitePlace.Completion.WithAbs

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ratCast_equiv 📖	mathematical	—	UniformSpace.Completion WithAbs Real Real.semiring Real.partialOrder DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Rat.instField AbsoluteValue RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithAbs.normedField DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NumberField.InfinitePlace.Completion.instNormedField DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring WithAbs.instSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike WithAbs.equiv UniformSpace.Completion.coe'	—	Complex.instNontrivial eq_ratCast RingHom.instRingHomClass

NumberField.InfinitePlace.LiesOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
embedding_liesOver_of_isReal 📖	mathematical	NumberField.InfinitePlace.IsReal	NumberField.ComplexEmbedding.LiesOver NumberField.InfinitePlace.embedding	—	DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Complex.instNontrivial NumberField.InfinitePlace.comap_embedding_of_isReal comap_eq
extensionEmbedding_liesOver_of_isReal 📖	mathematical	NumberField.InfinitePlace.IsReal	NumberField.ComplexEmbedding.LiesOver NumberField.InfinitePlace.Completion NormedField.toField NumberField.InfinitePlace.Completion.instNormedField NumberField.InfinitePlace.Completion.extensionEmbedding	—	DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Complex.instNontrivial NumberField.InfinitePlace.Completion.liesOver_extensionEmbedding embedding_liesOver_of_isReal
isometry_algebraMap 📖	mathematical	—	Isometry 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 EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace WithAbs.normedField DFunLike.coe CommSemiring.toSemiring WithAbs.instCommSemiring Semifield.toCommSemiring WithAbs.instSemiring RingHom.instFunLike algebraMap WithAbs.algebraLeft WithAbs.instAlgebra	—	DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Complex.instNontrivial AddMonoidHomClass.isometry_of_norm RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass NumberField.InfinitePlace.comp_of_comap_eq comap_eq WithAbs.ofAbs_algebraMap

---

← Back to Index