NormLeOne

📁 Source: Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

Statistics

Metric	Count
Definitions compactSet, completeBasis, completeFamily, deriv_expMap_single, equivFinRank, expMap, expMapBasis, expMap_single, fderiv_expMap, fderiv_expMapBasis, normLeOne, paramSet, realSpaceToLogSpace	13
Theorems abs_det_completeBasis_equivFunL_symm, abs_det_fderiv_expMapBasis, closure_normLeOne_subset, closure_paramSet, closure_paramSet_ae_interior, compactSet_ae, compactSet_eq_union, compactSet_eq_union_aux₁, compactSet_eq_union_aux₂, completeBasis_apply_of_eq, completeBasis_apply_of_ne, continuous_expMap, continuous_expMapBasis, expMapBasis_apply, expMapBasis_apply', expMapBasis_apply'', expMapBasis_closure_subset_compactSet, expMapBasis_nonneg, expMapBasis_pos, expMapBasis_source, expMap_add, expMap_apply, expMap_basis_of_eq, expMap_basis_of_ne, expMap_pos, expMap_single_apply, expMap_single_source, expMap_single_symm_apply, expMap_single_target, expMap_smul, expMap_source, expMap_sum, expMap_symm_apply, expMap_target, hasDerivAt_expMap_single, hasFDerivAt_expMap, hasFDerivAt_expMapBasis, injective_expMap, injective_expMapBasis, interior_paramSet, isBounded_normLeOne, isCompact_compactSet, linearIndependent_completeFamily, logMap_expMap, logMap_expMapBasis, logMap_normAtAllPlaces, measurableSet_interior_paramSet, measurableSet_normLeOne, measurableSet_paramSet, mem_normLeOne, nonneg_of_mem_compactSet, normAtAllPlaces_image_preimage_expMapBasis, normAtAllPlaces_mem_fundamentalCone_iff, normAtAllPlaces_normLeOne, normAtAllPlaces_normLeOne_eq_image, normLeOne_eq_preimage, normLeOne_eq_preimage_image, norm_expMapBasis, norm_expMapBasis_ne_zero, norm_normAtAllPlaces, prod_deriv_expMap_single, prod_expMapBasis_pow, realSpaceToLogSpace_apply, realSpaceToLogSpace_completeFamily_of_eq, realSpaceToLogSpace_completeFamily_of_ne, realSpaceToLogSpace_expMap_symm, setLIntegral_expMapBasis_image, setLIntegral_paramSet_exp, subset_interior_normLeOne, sum_eq_zero_of_mem_span_completeFamily, sum_expMap_symm_apply, volume_frontier_normLeOne, volume_interior_eq_volume_closure, volume_normLeOne, zero_mem_compactSet	75
Total	88

NumberField.mixedEmbedding.fundamentalCone

Definitions

Name	Category	Theorems
compactSet 📖	CompOp	7 math math: isCompact_compactSet, expMapBasis_closure_subset_compactSet, closure_normLeOne_subset, compactSet_eq_union_aux₂, compactSet_ae, zero_mem_compactSet, compactSet_eq_union
completeBasis 📖	CompOp	7 math math: abs_det_completeBasis_equivFunL_symm, completeBasis_apply_of_ne, prod_deriv_expMap_single, completeBasis_apply_of_eq, expMap_basis_of_eq, expMapBasis_apply, expMap_basis_of_ne
completeFamily 📖	CompOp	3 math math: realSpaceToLogSpace_completeFamily_of_ne, realSpaceToLogSpace_completeFamily_of_eq, linearIndependent_completeFamily
deriv_expMap_single 📖	CompOp	2 math math: prod_deriv_expMap_single, hasDerivAt_expMap_single
equivFinRank 📖	CompOp	4 math math: expMapBasis_apply', realSpaceToLogSpace_completeFamily_of_ne, completeBasis_apply_of_ne, expMap_basis_of_ne
expMap 📖	CompOp	17 math math: completeBasis_apply_of_ne, expMap_target, expMap_basis_of_eq, continuous_expMap, expMap_smul, hasFDerivAt_expMap, expMap_symm_apply, expMap_apply, expMap_source, expMap_add, expMapBasis_apply, realSpaceToLogSpace_expMap_symm, sum_expMap_symm_apply, expMap_sum, expMap_pos, injective_expMap, expMap_basis_of_ne
expMapBasis 📖	CompOp	23 math math: expMapBasis_apply', compactSet_eq_union_aux₁, logMap_expMapBasis, subset_interior_normLeOne, prod_deriv_expMap_single, norm_expMapBasis, prod_expMapBasis_pow, expMapBasis_closure_subset_compactSet, continuous_expMapBasis, hasFDerivAt_expMapBasis, expMapBasis_pos, injective_expMapBasis, expMapBasis_apply'', expMapBasis_apply, setLIntegral_expMapBasis_image, compactSet_ae, abs_det_fderiv_expMapBasis, normAtAllPlaces_image_preimage_expMapBasis, normAtAllPlaces_normLeOne_eq_image, expMapBasis_source, normLeOne_eq_preimage, compactSet_eq_union, expMapBasis_nonneg
expMap_single 📖	CompOp	5 math math: hasDerivAt_expMap_single, expMap_single_symm_apply, expMap_single_apply, expMap_single_source, expMap_single_target
fderiv_expMap 📖	CompOp	1 math math: hasFDerivAt_expMap
fderiv_expMapBasis 📖	CompOp	2 math math: hasFDerivAt_expMapBasis, abs_det_fderiv_expMapBasis
normLeOne 📖	CompOp	12 math math: volume_frontier_normLeOne, volume_interior_eq_volume_closure, subset_interior_normLeOne, mem_normLeOne, normLeOne_eq_preimage_image, closure_normLeOne_subset, isBounded_normLeOne, volume_normLeOne, normAtAllPlaces_normLeOne_eq_image, measurableSet_normLeOne, normLeOne_eq_preimage, normAtAllPlaces_normLeOne
paramSet 📖	CompOp	12 math math: interior_paramSet, compactSet_eq_union_aux₁, subset_interior_normLeOne, expMapBasis_closure_subset_compactSet, closure_paramSet, setLIntegral_paramSet_exp, compactSet_ae, normAtAllPlaces_normLeOne_eq_image, measurableSet_paramSet, normLeOne_eq_preimage, compactSet_eq_union, closure_paramSet_ae_interior
realSpaceToLogSpace 📖	CompOp	4 math math: realSpaceToLogSpace_completeFamily_of_ne, realSpaceToLogSpace_completeFamily_of_eq, realSpaceToLogSpace_apply, realSpaceToLogSpace_expMap_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_det_completeBasis_equivFunL_symm 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup ContinuousLinearMap.det Real.commRing Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Pi.addCommGroup Real.instAddCommGroup Pi.Function.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace ContinuousLinearEquiv.toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NumberField.mixedEmbedding.realSpace Real.pseudoMetricSpace AddCommGroup.toAddCommMonoid Real.semiring Real.instAddCommMonoid Real.normedField Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearEquiv.symm Module.Basis.equivFunL Pi.topologicalAddGroup AddCommGroup.toAddGroup instIsTopologicalAddGroupReal instContinuousSMulForall SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction IsModuleTopology.toContinuousSMul Real.instAdd Algebra.toSMul Real.instCommSemiring Algebra.id IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing instIsTopologicalRingReal Real.instCompleteSpace Finite.of_fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace Real.metricSpace completeBasis Real.instMul Real.instNatCast Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Rat.commSemiring DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero NumberField.Units.regulator	—	RingHomInvPair.ids Pi.topologicalAddGroup instIsTopologicalAddGroupReal instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.instCompleteSpace Finite.of_fintype Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace NumberField.to_charZero ContinuousLinearMap.det.eq_1 smulCommClass_self LinearMap.det_toMatrix Matrix.det_transpose NumberField.Units.regulator_eq_regOfFamily_fundSystem NumberField.Units.finrank_mul_regOfFamily_eq_det Matrix.ext Matrix.transpose_apply LinearMap.toMatrix_apply Matrix.of_apply Module.Basis.equivFunL_apply ContinuousLinearMap.coe_coe ContinuousLinearEquiv.coe_apply ContinuousLinearEquiv.apply_symm_apply completeBasis_apply_of_eq completeBasis_apply_of_ne NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding
abs_det_fderiv_expMapBasis 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup ContinuousLinearMap.det Real.commRing NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommGroup Real.instAddCommGroup Pi.Function.module Real.semiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal fderiv_expMapBasis Real.instMul Real.exp NumberField.Units.dirichletUnitTheorem.w₀ Real.instNatCast Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero Real.instInv Finset.prod NumberField.InfinitePlace.IsComplex Real.instCommMonoid Finset.univ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype OpenPartialHomeomorph.toFun' expMapBasis Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat NumberField.InfinitePlace.nrComplexPlaces NumberField.Units.regulator	—	NumberField.to_charZero Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids Real.instCompleteSpace LinearMap.det_comp LinearMap.det_pi Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Real.instIsDomain FiniteDimensional.rclike_to_real instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Finset.prod_congr LinearMap.det_ring one_smul abs_mul Real.instIsOrderedRing abs_det_completeBasis_equivFunL_symm prod_deriv_expMap_single Real.exp_mul abs_pow Real.rpow_natCast abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.exp_nonneg abs_inv Real.instIsStrictOrderedRing Finset.abs_prod expMapBasis_nonneg Nat.abs_ofNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Tactic.Ring.pow_prod_atom
closure_normLeOne_subset 📖	mathematical	—	Set NumberField.mixedEmbedding.mixedSpace Set.instHasSubset closure instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField normLeOne Set.preimage NumberField.mixedEmbedding.realSpace NumberField.mixedEmbedding.normAtAllPlaces compactSet	—	normLeOne_eq_preimage HasSubset.Subset.trans Set.instIsTransSubset Continuous.closure_preimage_subset NumberField.mixedEmbedding.continuous_normAtAllPlaces Set.preimage_mono IsClosed.closure_subset_iff IsCompact.isClosed Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace isCompact_compactSet Set.image_mono subset_closure expMapBasis_closure_subset_compactSet
closure_paramSet 📖	mathematical	—	closure NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace paramSet Set.pi Set.univ Set NumberField.Units.dirichletUnitTheorem.w₀ Set.Iic Real.instPreorder Real.instZero Set.Icc Real.instOne	—	closure_pi_set closure_Iic instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid closure_Ico instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing NeZero.charZero_one RCLike.charZero_rclike
closure_paramSet_ae_interior 📖	mathematical	—	Filter.EventuallyEq NumberField.mixedEmbedding.realSpace MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume closure Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace paramSet interior	—	MeasureTheory.Measure.instOuterMeasureClass closure_paramSet interior_paramSet MeasureTheory.volume_pi MeasureTheory.Measure.ae_eq_set_pi MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Filter.EventuallyEq.symm MeasureTheory.Iio_ae_eq_Iic Real.noAtoms_volume MeasureTheory.Ioo_ae_eq_Icc
compactSet_ae 📖	mathematical	—	Filter.EventuallyEq NumberField.mixedEmbedding.realSpace MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume compactSet Set.image OpenPartialHomeomorph.toFun' Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis closure paramSet	—	MeasureTheory.Measure.instOuterMeasureClass compactSet_eq_union MeasureTheory.union_ae_eq_left_of_ae_eq_empty MeasureTheory.NoAtoms.measure_singleton MeasureTheory.Measure.instNoAtomsForallVolumeOfNonemptyOfSigmaFinite NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Real.noAtoms_volume
compactSet_eq_union 📖	mathematical	—	compactSet Set NumberField.mixedEmbedding.realSpace Set.instUnion Set.image OpenPartialHomeomorph.toFun' Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis closure paramSet Set.instSingletonSet Pi.instZero Real.instZero	—	Set.ext Set.union_singleton zero_mem_compactSet Set.mem_union_left compactSet_eq_union_aux₁ compactSet_eq_union_aux₂
compactSet_eq_union_aux₁ 📖	mathematical	NumberField.mixedEmbedding.realSpace Set Set.instMembership compactSet	Set.image OpenPartialHomeomorph.toFun' Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis closure paramSet	—	closure_paramSet Set.mem_univ_pi Real.log_nonpos Set.mem_univ Mathlib.Tactic.Contrapose.contrapose₂ le_antisymm zero_smul expMapBasis_apply'' Real.exp_log
compactSet_eq_union_aux₂ 📖	mathematical	NumberField.mixedEmbedding.realSpace Set Set.instMembership Set.image OpenPartialHomeomorph.toFun' Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis closure paramSet	compactSet	—	closure_paramSet Real.exp_nonneg Real.exp_le_one_iff Set.mem_univ Set.mem_univ_pi expMapBasis_apply''
completeBasis_apply_of_eq 📖	mathematical	—	DFunLike.coe Module.Basis NumberField.InfinitePlace Real NumberField.mixedEmbedding.realSpace Real.semiring Pi.addCommMonoid Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Module.Basis.instFunLike completeBasis NumberField.Units.dirichletUnitTheorem.w₀ Real.instNatCast NumberField.InfinitePlace.mult	—	linearIndependent_completeFamily completeBasis.eq_1 coe_basisOfLinearIndependentOfCardEqFinrank completeFamily.eq_1
completeBasis_apply_of_ne 📖	mathematical	—	DFunLike.coe Module.Basis NumberField.InfinitePlace Real NumberField.mixedEmbedding.realSpace Real.semiring Pi.addCommMonoid Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Module.Basis.instFunLike completeBasis NumberField.Units.dirichletUnitTheorem.w₀ OpenPartialHomeomorph.toFun' Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm expMap NumberField.mixedEmbedding.normAtAllPlaces RingHom NumberField.mixedEmbedding.mixedSpace Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero NumberField.Units.fundSystem Equiv NumberField.Units.rank EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivFinRank	—	linearIndependent_completeFamily completeBasis.eq_1 coe_basisOfLinearIndependentOfCardEqFinrank completeFamily.eq_1
continuous_expMap 📖	mathematical	—	Continuous NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.toFun' expMap	—	continuousOn_univ OpenPartialHomeomorph.continuousOn expMap_source
continuous_expMapBasis 📖	mathematical	—	Continuous NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.toFun' expMapBasis	—	Continuous.comp Real.instCompleteSpace continuous_expMap ContinuousLinearEquiv.continuous
expMapBasis_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis expMap DFunLike.coe LinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Real.instAddCommMonoid Pi.Function.module Semiring.toModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm Module.Basis.equivFun Finite.of_fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype completeBasis	—	—
expMapBasis_apply' 📖	mathematical	—	OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.exp NumberField.Units.dirichletUnitTheorem.w₀ Finset.prod Real.instCommMonoid Finset.univ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.instPow DFunLike.coe NumberField.InfinitePlace.instFunLikeReal RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero NumberField.Units.fundSystem Equiv NumberField.Units.rank EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivFinRank	—	RingHomInvPair.ids Finite.of_fintype Module.Basis.equivFun_symm_apply Fintype.sum_eq_add_sum_subtype_ne expMap_add expMap_smul expMap_basis_of_eq Real.exp_one_rpow expMap_sum Finset.prod_congr expMap_basis_of_ne Finset.prod_apply NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding
expMapBasis_apply'' 📖	mathematical	—	OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.exp NumberField.Units.dirichletUnitTheorem.w₀ Real.instZero	—	expMapBasis_apply' smul_smul Real.exp_add add_zero Subtype.prop
expMapBasis_closure_subset_compactSet 📖	mathematical	—	Set NumberField.mixedEmbedding.realSpace Set.instHasSubset Set.image OpenPartialHomeomorph.toFun' Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis closure paramSet compactSet	—	compactSet_eq_union Set.subset_union_left
expMapBasis_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis	—	LT.lt.le expMapBasis_pos
expMapBasis_pos 📖	mathematical	—	Real Real.instLT Real.instZero OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis	—	expMap_pos Real.instCompleteSpace
expMapBasis_source 📖	mathematical	—	PartialEquiv.source NumberField.mixedEmbedding.realSpace OpenPartialHomeomorph.toPartialEquiv Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis Set.univ	—	Real.instCompleteSpace expMap_source
expMap_add 📖	mathematical	—	OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap Pi.instAdd Real.instAdd Pi.instMul Real.instMul	—	mul_add Distrib.leftDistribClass Real.exp_add
expMap_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap Real.exp Real.instMul Real.instInv Real.instNatCast NumberField.InfinitePlace.mult	—	—
expMap_basis_of_eq 📖	mathematical	—	OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap DFunLike.coe Module.Basis Real.semiring Pi.addCommMonoid Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Module.Basis.instFunLike completeBasis NumberField.Units.dirichletUnitTheorem.w₀ Real.exp Real.instOne	—	completeBasis_apply_of_eq inv_mul_cancel₀ NumberField.InfinitePlace.mult_coe_ne_zero
expMap_basis_of_ne 📖	mathematical	—	OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap DFunLike.coe Module.Basis Real.semiring Pi.addCommMonoid Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Module.Basis.instFunLike completeBasis NumberField.Units.dirichletUnitTheorem.w₀ NumberField.mixedEmbedding.normAtAllPlaces RingHom NumberField.mixedEmbedding.mixedSpace Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero NumberField.Units.fundSystem Equiv NumberField.Units.rank EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivFinRank	—	completeBasis_apply_of_ne OpenPartialHomeomorph.right_inv expMap_target NumberField.mixedEmbedding.normAtPlace_apply
expMap_pos 📖	mathematical	—	Real Real.instLT Real.instZero OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap	—	Real.exp_pos
expMap_single_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap_single Real.exp Real.instMul Real.instInv Real.instNatCast NumberField.InfinitePlace.mult	—	—
expMap_single_source 📖	mathematical	—	PartialEquiv.source Real OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap_single Set.univ	—	—
expMap_single_symm_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm expMap_single Real.instMul Real.instNatCast NumberField.InfinitePlace.mult Real.log	—	—
expMap_single_target 📖	mathematical	—	PartialEquiv.target Real OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap_single Set.Ioi Real.instPreorder Real.instZero	—	—
expMap_smul 📖	mathematical	—	OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Pi.instPow Real.instPow	—	mul_comm Real.exp_mul
expMap_source 📖	mathematical	—	PartialEquiv.source NumberField.mixedEmbedding.realSpace OpenPartialHomeomorph.toPartialEquiv Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap Set.univ	—	Set.pi_univ
expMap_sum 📖	mathematical	—	OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap Finset.sum Pi.addCommMonoid Real.instAddCommMonoid Finset.prod Pi.commMonoid Real.instCommMonoid	—	Finset.sum_apply Finset.prod_apply Finset.prod_congr
expMap_symm_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm expMap Real.instMul Real.instNatCast NumberField.InfinitePlace.mult Real.log	—	—
expMap_target 📖	mathematical	—	PartialEquiv.target NumberField.mixedEmbedding.realSpace OpenPartialHomeomorph.toPartialEquiv Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap Set.pi Set.univ Set.Ioi Real.instPreorder Real.instZero	—	—
hasDerivAt_expMap_single 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal OpenPartialHomeomorph.toFun' expMap_single deriv_expMap_single	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.congr_simp mul_comm IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.comp Real.hasDerivAt_exp hasDerivAt_mul_const
hasFDerivAt_expMap 📖	mathematical	—	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NumberField.mixedEmbedding.realSpace Pi.addCommGroup NumberField.InfinitePlace Real.instAddCommGroup Pi.Function.module Real.semiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.toFun' expMap fderiv_expMap	—	Finite.of_fintype HasFDerivAt.comp IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.hasFDerivAt hasDerivAt_expMap_single hasFDerivAt_apply
hasFDerivAt_expMapBasis 📖	mathematical	—	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NumberField.mixedEmbedding.realSpace Pi.addCommGroup NumberField.InfinitePlace Real.instAddCommGroup Pi.Function.module Real.semiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.toFun' expMapBasis fderiv_expMapBasis	—	HasFDerivAt.comp RingHomInvPair.ids Pi.topologicalAddGroup instIsTopologicalAddGroupReal instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.instCompleteSpace Finite.of_fintype Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivAt_expMap ContinuousLinearEquiv.hasFDerivAt
injective_expMap 📖	mathematical	—	NumberField.mixedEmbedding.realSpace OpenPartialHomeomorph.toFun' Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMap	—	Set.injOn_univ OpenPartialHomeomorph.injOn expMap_source
injective_expMapBasis 📖	mathematical	—	NumberField.mixedEmbedding.realSpace OpenPartialHomeomorph.toFun' Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis	—	Real.instCompleteSpace injective_expMap LinearEquiv.injective RingHomInvPair.ids Finite.of_fintype
interior_paramSet 📖	mathematical	—	interior NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace paramSet Set.pi Set.univ Set NumberField.Units.dirichletUnitTheorem.w₀ Set.Iio Real.instPreorder Real.instZero Set.Ioo Real.instOne	—	interior_pi_set Set.finite_univ Finite.of_fintype interior_Iic' instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial interior_Ico instNoMinOrderOfNontrivial
isBounded_normLeOne 📖	mathematical	—	Bornology.IsBounded NumberField.mixedEmbedding.mixedSpace Prod.instBornology Pi.instBornology NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField normLeOne	—	normLeOne_eq_preimage Bornology.IsBounded.subset IsCompact.isBounded isCompact_compactSet expMapBasis_closure_subset_compactSet Set.image_mono subset_closure isBounded_iff_forall_norm_le Finset.univ_nonempty NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace Finset.sup'_le Real.norm_of_nonneg NumberField.mixedEmbedding.normAtPlace_nonneg pi_norm_le_iff_of_nonempty
isCompact_compactSet 📖	mathematical	—	IsCompact NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace compactSet	—	IsCompact.smul_set instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal IsCompact.image_of_continuousOn isCompact_univ_pi isCompact_singleton Continuous.continuousOn continuous_expMapBasis
linearIndependent_completeFamily 📖	mathematical	—	LinearIndependent NumberField.InfinitePlace Real NumberField.mixedEmbedding.realSpace completeFamily Real.semiring Pi.addCommMonoid Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal	—	LinearIndependent.of_comp realSpaceToLogSpace_completeFamily_of_ne Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice Module.Basis.coe_reindex Module.Basis.ofZLatticeBasis_apply Module.Basis.linearIndependent sum_eq_zero_of_mem_span_completeFamily LT.lt.ne' NumberField.to_charZero Module.finrank_pos commRing_strongRankCondition Rat.nontrivial NumberField.to_finiteDimensional Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing Nat.cast_eq_zero RCLike.charZero_rclike NumberField.InfinitePlace.sum_mult_eq Nat.cast_sum completeFamily.eq_1 linearIndependent_equiv linearIndependent_option
logMap_expMap 📖	mathematical	DFunLike.coe MonoidWithZeroHom NumberField.mixedEmbedding.mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike NumberField.mixedEmbedding.norm ContinuousLinearMap RingHom.id NumberField.mixedEmbedding.realSpace Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid instTopologicalSpaceProd SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Prod.instModule instInnerProductSpaceRealComplex ContinuousLinearMap.funLike NumberField.mixedEmbedding.mixedSpaceOfRealSpace OpenPartialHomeomorph.toFun' expMap Real.instOne	NumberField.mixedEmbedding.logMap NumberField.Units.dirichletUnitTheorem.w₀	—	NumberField.to_charZero NumberField.mixedEmbedding.logMap.eq_1 NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace Real.exp_nonneg expMap_apply Real.log_exp mul_sub mul_inv_cancel_left₀ NumberField.InfinitePlace.mult_coe_ne_zero Real.log_one MulZeroClass.zero_mul MulZeroClass.mul_zero sub_zero
logMap_expMapBasis 📖	mathematical	—	NumberField.Units.dirichletUnitTheorem.logSpace Set Set.instMembership ZSpan.fundamentalDomain NumberField.Units.rank Real Real.normedField Pi.normedAddCommGroup NumberField.InfinitePlace NumberField.Units.dirichletUnitTheorem.w₀ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Module.Basis.ofZLatticeBasis Real.linearOrder Real.instIsStrictOrderedRing instHasSolidNormReal Real.instFloorRing FiniteDimensional.finiteDimensional_pi' NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Subtype.finite Finite.of_fintype Real.instAddCommGroup NormedSpace.toModule FiniteDimensional.rclike_to_real pi_properSpace SeminormedAddGroup.toPseudoMetricSpace instProperSpaceReal NumberField.Units.unitLattice NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice NumberField.Units.basisUnitLattice NumberField.mixedEmbedding.logMap DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring NumberField.mixedEmbedding.realSpace Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid NumberField.mixedEmbedding.mixedSpace instTopologicalSpaceProd NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module Prod.instModule instInnerProductSpaceRealComplex ContinuousLinearMap.funLike NumberField.mixedEmbedding.mixedSpaceOfRealSpace OpenPartialHomeomorph.toFun' expMapBasis Set.Ico Real.instPreorder Real.instZero Real.instOne	—	Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice RingHomInvPair.ids Equiv.forall_congr_left expMapBasis_apply'' map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass NumberField.mixedEmbedding.logMap_real_smul norm_expMapBasis_ne_zero Real.exp_ne_zero expMapBasis_apply logMap_expMap NumberField.to_charZero norm_expMapBasis Real.exp_zero one_pow Module.Basis.equivFun_symm_apply Fintype.sum_eq_add_sum_subtype_ne zero_smul zero_add Subtype.prop Finset.sum_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finset.sum_congr completeBasis_apply_of_ne NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding NumberField.Units.logEmbedding_fundSystem Finsupp.coe_finset_sum Module.Basis.ofZLatticeBasis_repr_apply Module.Basis.repr_self Finsupp.single_apply EquivLike.toEmbeddingLike Int.cast_ite Int.cast_one Int.cast_zero smul_ite mul_one MulZeroClass.mul_zero Fintype.sum_ite_eq'
logMap_normAtAllPlaces 📖	mathematical	—	NumberField.mixedEmbedding.logMap DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid NumberField.mixedEmbedding.mixedSpace instTopologicalSpaceProd NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Prod.instModule instInnerProductSpaceRealComplex ContinuousLinearMap.funLike NumberField.mixedEmbedding.mixedSpaceOfRealSpace NumberField.mixedEmbedding.normAtAllPlaces	—	NumberField.mixedEmbedding.logMap_eq_of_normAtPlace_eq NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace NumberField.mixedEmbedding.normAtPlace_nonneg
measurableSet_interior_paramSet 📖	mathematical	—	MeasurableSet interior	—	measurableSet_interior
measurableSet_normLeOne 📖	mathematical	—	MeasurableSet NumberField.mixedEmbedding.mixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace normLeOne	—	MeasurableSet.inter NumberField.mixedEmbedding.measurableSet_fundamentalCone measurableSet_le BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid instSecondCountableTopologyReal Continuous.measurable Prod.opensMeasurableSpace Pi.opensMeasurableSpace Subtype.countable Finite.to_countable Finite.of_fintype secondCountable_of_proper Complex.instProperSpace Complex.borelSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable NumberField.mixedEmbedding.continuous_norm measurable_const
measurableSet_paramSet 📖	mathematical	—	MeasurableSet NumberField.mixedEmbedding.realSpace MeasurableSpace.pi NumberField.InfinitePlace Real Real.measurableSpace paramSet	—	MeasurableSet.univ_pi Finite.to_countable Finite.of_fintype measurableSet_Iic BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid measurableSet_Ico instClosedIciTopology
mem_normLeOne 📖	mathematical	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership normLeOne NumberField.mixedEmbedding.fundamentalCone Real Real.instLE DFunLike.coe MonoidWithZeroHom Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike NumberField.mixedEmbedding.norm Real.instOne	—	Set.mem_sep_iff
nonneg_of_mem_compactSet 📖	mathematical	NumberField.mixedEmbedding.realSpace Set Set.instMembership compactSet	Real Real.instLE Real.instZero	—	mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le expMapBasis_pos
normAtAllPlaces_image_preimage_expMapBasis 📖	mathematical	—	Set.image NumberField.mixedEmbedding.mixedSpace NumberField.mixedEmbedding.realSpace NumberField.mixedEmbedding.normAtAllPlaces Set.preimage OpenPartialHomeomorph.toFun' Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis	—	NumberField.mixedEmbedding.normAtAllPlaces_image_preimage_of_nonneg LT.lt.le expMapBasis_pos
normAtAllPlaces_mem_fundamentalCone_iff 📖	mathematical	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership NumberField.mixedEmbedding.fundamentalCone DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring NumberField.mixedEmbedding.realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid instTopologicalSpaceProd NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Prod.instModule instInnerProductSpaceRealComplex ContinuousLinearMap.funLike NumberField.mixedEmbedding.mixedSpaceOfRealSpace NumberField.mixedEmbedding.normAtAllPlaces	—	Real.instIsStrictOrderedRing instHasSolidNormReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice logMap_normAtAllPlaces norm_normAtAllPlaces
normAtAllPlaces_normLeOne 📖	mathematical	—	Set.image NumberField.mixedEmbedding.mixedSpace NumberField.mixedEmbedding.realSpace NumberField.mixedEmbedding.normAtAllPlaces normLeOne Set Set.instInter Set.preimage DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid instTopologicalSpaceProd NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Prod.instModule instInnerProductSpaceRealComplex ContinuousLinearMap.funLike NumberField.mixedEmbedding.mixedSpaceOfRealSpace NumberField.Units.dirichletUnitTheorem.logSpace NumberField.mixedEmbedding.logMap ZSpan.fundamentalDomain NumberField.Units.rank Pi.normedAddCommGroup NumberField.Units.dirichletUnitTheorem.w₀ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup Pi.normedSpace Module.Basis.ofZLatticeBasis Real.linearOrder Real.instIsStrictOrderedRing instHasSolidNormReal Real.instFloorRing FiniteDimensional.finiteDimensional_pi' NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Subtype.finite Finite.of_fintype Real.instAddCommGroup FiniteDimensional.rclike_to_real pi_properSpace SeminormedAddGroup.toPseudoMetricSpace instProperSpaceReal NumberField.Units.unitLattice NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice NumberField.Units.basisUnitLattice setOf MonoidWithZeroHom Prod.instMulZeroOneClass Pi.mulZeroOneClass NonAssocSemiring.toMulZeroOneClass Complex.instSemiring MonoidWithZeroHom.funLike NumberField.mixedEmbedding.norm Real.instZero Real.instLE Real.instOne	—	Set.ext Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice logMap_normAtAllPlaces Set.mem_preimage NumberField.mixedEmbedding.normAtPlace_nonneg norm_normAtAllPlaces Set.mem_setOf_eq NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace
normAtAllPlaces_normLeOne_eq_image 📖	mathematical	—	Set.image NumberField.mixedEmbedding.mixedSpace NumberField.mixedEmbedding.realSpace NumberField.mixedEmbedding.normAtAllPlaces normLeOne OpenPartialHomeomorph.toFun' Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis paramSet	—	Set.ext OpenPartialHomeomorph.right_inv Set.mem_univ_pi Function.Injective.mem_set_image injective_expMapBasis Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice normAtAllPlaces_normLeOne NumberField.to_charZero norm_expMapBasis isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.instNontrivial pow_le_one_iff_of_nonneg IsStrictOrderedRing.toPosMulStrictMono Real.instZeroLEOneClass Real.exp_nonneg LT.lt.ne' Module.finrank_pos commRing_strongRankCondition Rat.nontrivial NumberField.to_finiteDimensional Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing normAtPlace_pos_of_mem expMapBasis_pos
normLeOne_eq_preimage 📖	mathematical	—	normLeOne Set.preimage NumberField.mixedEmbedding.mixedSpace NumberField.mixedEmbedding.realSpace NumberField.mixedEmbedding.normAtAllPlaces Set.image OpenPartialHomeomorph.toFun' Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis paramSet	—	normLeOne_eq_preimage_image normAtAllPlaces_normLeOne_eq_image
normLeOne_eq_preimage_image 📖	mathematical	—	normLeOne Set.preimage NumberField.mixedEmbedding.mixedSpace NumberField.mixedEmbedding.realSpace NumberField.mixedEmbedding.normAtAllPlaces Set.image	—	subset_antisymm Set.instAntisymmSubset Set.subset_preimage_image mem_normLeOne normAtAllPlaces_mem_fundamentalCone_iff norm_normAtAllPlaces
norm_expMapBasis 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom NumberField.mixedEmbedding.mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike NumberField.mixedEmbedding.norm ContinuousLinearMap RingHom.id NumberField.mixedEmbedding.realSpace Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid instTopologicalSpaceProd SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Prod.instModule instInnerProductSpaceRealComplex ContinuousLinearMap.funLike NumberField.mixedEmbedding.mixedSpaceOfRealSpace OpenPartialHomeomorph.toFun' expMapBasis Monoid.toNatPow Real.instMonoid Real.exp NumberField.Units.dirichletUnitTheorem.w₀ Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	NumberField.to_charZero Finset.prod_congr NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace LT.lt.le expMapBasis_pos prod_expMapBasis_pow
norm_expMapBasis_ne_zero 📖	—	—	—	—	NumberField.to_charZero pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.exp_ne_zero norm_expMapBasis
norm_normAtAllPlaces 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom NumberField.mixedEmbedding.mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike NumberField.mixedEmbedding.norm ContinuousLinearMap RingHom.id NumberField.mixedEmbedding.realSpace Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid instTopologicalSpaceProd SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Prod.instModule instInnerProductSpaceRealComplex ContinuousLinearMap.funLike NumberField.mixedEmbedding.mixedSpaceOfRealSpace NumberField.mixedEmbedding.normAtAllPlaces	—	Finset.prod_congr NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace NumberField.mixedEmbedding.normAtAllPlaces_nonneg
prod_deriv_expMap_single 📖	mathematical	—	Finset.prod NumberField.InfinitePlace Real Real.instCommMonoid Finset.univ NumberField.InfinitePlace.NumberField.InfinitePlace.fintype deriv_expMap_single DFunLike.coe LinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NumberField.mixedEmbedding.realSpace Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Real.instAddCommMonoid Pi.Function.module Semiring.toModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm Module.Basis.equivFun Finite.of_fintype completeBasis Real.instMul Monoid.toNatPow Real.instMonoid Real.exp NumberField.Units.dirichletUnitTheorem.w₀ Module.finrank Rat.semiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero Real.instInv NumberField.InfinitePlace.IsComplex Subtype.fintype OpenPartialHomeomorph.toFun' Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat NumberField.InfinitePlace.nrComplexPlaces	—	RingHomInvPair.ids Finite.of_fintype NumberField.to_charZero Nat.instAtLeastTwoHAddOfNat Finset.prod_congr Finset.prod_mul_distrib NumberField.InfinitePlace.prod_eq_prod_mul_prod NumberField.InfinitePlace.mult_isReal NumberField.InfinitePlace.mult_isComplex pow_one Finset.prod_pow pow_two mul_assoc mul_inv_cancel₀ Finset.prod_ne_zero_iff Real.instNontrivial NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.exp_ne_zero mul_one Finset.prod_inv_distrib Nat.cast_one Finset.prod_const_one Finset.prod_const one_mul inv_pow
prod_expMapBasis_pow 📖	mathematical	—	Finset.prod NumberField.InfinitePlace Real Real.instCommMonoid Finset.univ NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Monoid.toNatPow Real.instMonoid OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis NumberField.InfinitePlace.mult Real.exp NumberField.Units.dirichletUnitTheorem.w₀ Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	NumberField.to_charZero Finset.prod_congr expMapBasis_apply' mul_pow Finset.prod_mul_distrib Finset.prod_pow_eq_pow_sum NumberField.InfinitePlace.sum_mult_eq Finset.prod_comm Real.rpow_pow_comm NonnegHomClass.apply_nonneg NumberField.InfinitePlace.instNonnegHomClassReal Real.finset_prod_rpow pow_nonneg Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing NumberField.InfinitePlace.prod_eq_abs_norm NumberField.Units.norm Rat.cast_one Real.one_rpow Finset.prod_const_one mul_one
realSpaceToLogSpace_apply 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring NumberField.mixedEmbedding.realSpace Pi.addCommMonoid NumberField.InfinitePlace Real.instAddCommMonoid NumberField.Units.dirichletUnitTheorem.w₀ Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal LinearMap.instFunLike realSpaceToLogSpace Real.instSub Real.instMul Real.instNatCast NumberField.InfinitePlace.mult Finset.sum Finset.univ NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.instInv Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	—
realSpaceToLogSpace_completeFamily_of_eq 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring NumberField.mixedEmbedding.realSpace Pi.addCommMonoid NumberField.InfinitePlace Real.instAddCommMonoid NumberField.Units.dirichletUnitTheorem.w₀ Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal LinearMap.instFunLike realSpaceToLogSpace completeFamily Pi.instZero Real.instZero	—	NumberField.to_charZero realSpaceToLogSpace_apply completeFamily.eq_1 Nat.cast_sum NumberField.InfinitePlace.sum_mult_eq mul_inv_cancel_right₀ Nat.cast_ne_zero RCLike.charZero_rclike LT.lt.ne' Module.finrank_pos commRing_strongRankCondition Rat.nontrivial NumberField.to_finiteDimensional Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing sub_self Pi.zero_apply
realSpaceToLogSpace_completeFamily_of_ne 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring NumberField.mixedEmbedding.realSpace Pi.addCommMonoid NumberField.InfinitePlace Real.instAddCommMonoid NumberField.Units.dirichletUnitTheorem.w₀ Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal LinearMap.instFunLike realSpaceToLogSpace completeFamily NumberField.Units.dirichletUnitTheorem.logSpace Submodule Int.instSemiring AddCommGroup.toIntModule Pi.addCommGroup Real.instAddCommGroup SetLike.instMembership Submodule.setLike NumberField.Units.unitLattice Module.Basis NumberField.Units.rank Submodule.addCommMonoid Submodule.addCommGroup Int.instRing Module.Basis.instFunLike NumberField.Units.basisUnitLattice Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivFinRank	—	NumberField.Units.logEmbedding_fundSystem NumberField.mixedEmbedding.logMap_eq_logEmbedding completeFamily.eq_1 realSpaceToLogSpace_expMap_symm NumberField.Units.coe_ne_zero
realSpaceToLogSpace_expMap_symm 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring NumberField.mixedEmbedding.realSpace Pi.addCommMonoid NumberField.InfinitePlace Real.instAddCommMonoid NumberField.Units.dirichletUnitTheorem.w₀ Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal LinearMap.instFunLike realSpaceToLogSpace OpenPartialHomeomorph.toFun' Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm expMap NumberField.mixedEmbedding.normAtAllPlaces RingHom NumberField.mixedEmbedding.mixedSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.mixedEmbedding.logMap	—	NumberField.to_charZero sum_expMap_symm_apply NumberField.mixedEmbedding.normAtPlace_apply mul_sub mul_assoc NumberField.mixedEmbedding.norm_eq_norm
setLIntegral_expMapBasis_image 📖	mathematical	MeasurableSet NumberField.mixedEmbedding.realSpace MeasurableSpace.pi NumberField.InfinitePlace Real Real.measurableSpace Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.image OpenPartialHomeomorph.toFun' Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat NumberField.InfinitePlace.nrComplexPlaces ENNReal.ofReal NumberField.Units.regulator Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero Real.exp Real.instMul NumberField.Units.dirichletUnitTheorem.w₀ Real.instNatCast Finset.prod NumberField.InfinitePlace.IsComplex CommSemiring.toCommMonoid Finset.univ Subtype.fintype	—	Nat.instAtLeastTwoHAddOfNat NumberField.to_charZero MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real Pi.borelSpace Finite.to_countable instSecondCountableTopologyReal Real.borelSpace MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite ContinuousAdd.measurableAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal HasFDerivAt.hasFDerivWithinAt hasFDerivAt_expMapBasis Function.Injective.injOn injective_expMapBasis abs_det_fderiv_expMapBasis Continuous.measurable Pi.opensMeasurableSpace BorelSpace.opensMeasurable continuous_expMapBasis MeasureTheory.lintegral_const_mul Measurable.mul ENNReal.instMeasurableMul₂ Measurable.ennreal_ofReal Measurable.exp Measurable.mul_const ContinuousMul.measurableMul IsTopologicalSemiring.toContinuousMul measurable_pi_apply Measurable.inv ENNReal.instMeasurableInv Finset.measurable_prod Measurable.fun_comp inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Finset.prod_nonneg Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le expMapBasis_pos ENNReal.ofReal_mul mul_nonneg le_of_lt Real.exp_pos pow_pos IsStrictOrderedRing.toZeroLEOneClass inv_pos_of_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.ofReal_pow ENNReal.ofReal_inv_of_pos Finset.prod_pos zero_lt_two NeZero.charZero_one RCLike.charZero_rclike ENNReal.ofReal_ofNat ENNReal.ofReal_natCast ENNReal.ofReal_prod_of_nonneg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero
setLIntegral_paramSet_exp 📖	mathematical	—	MeasureTheory.lintegral NumberField.mixedEmbedding.realSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume paramSet ENNReal.ofReal Real.exp Real.instMul NumberField.Units.dirichletUnitTheorem.w₀ Real.instNatCast ENNReal ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial MeasureTheory.volume_pi paramSet.eq_1 MeasureTheory.Measure.restrict_pi_pi MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal MeasureTheory.lintegral_eq_lmarginal_univ MeasureTheory.Restrict.sigmaFinite MeasureTheory.lmarginal_erase' Measurable.ennreal_ofReal Measurable.exp Measurable.mul_const ContinuousMul.measurableMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal measurable_pi_apply Finset.mem_univ MeasureTheory.lmarginal.congr_simp Function.update_self MeasureTheory.lintegral_const MeasureTheory.Measure.pi_univ Finset.prod_congr Finset.ne_of_mem_erase Subtype.prop MeasureTheory.Measure.restrict_apply_univ Real.volume_Ico sub_zero ENNReal.ofReal_one Finset.prod_const_one mul_one mul_comm MeasureTheory.ofReal_integral_eq_lintegral_ofReal integrableOn_exp_mul_Iic Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass Real.exp_nonneg integral_exp_mul_Iic MulZeroClass.mul_zero Real.exp_zero ENNReal.ofReal_div_of_pos ENNReal.ofReal_natCast one_div
subset_interior_normLeOne 📖	mathematical	—	Set NumberField.mixedEmbedding.mixedSpace Set.instHasSubset Set.preimage NumberField.mixedEmbedding.realSpace NumberField.mixedEmbedding.normAtAllPlaces Set.image OpenPartialHomeomorph.toFun' Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace expMapBasis interior paramSet instTopologicalSpaceProd NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField normLeOne	—	normLeOne_eq_preimage subset_trans Set.instIsTransSubset Set.preimage_mono OpenPartialHomeomorph.isOpen_image_of_subset_source isOpen_interior expMapBasis_source interior_maximal Set.image_mono interior_subset preimage_interior_subset_interior_preimage NumberField.mixedEmbedding.continuous_normAtAllPlaces
sum_eq_zero_of_mem_span_completeFamily 📖	mathematical	NumberField.mixedEmbedding.realSpace Submodule Real Real.semiring Pi.addCommMonoid NumberField.InfinitePlace Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SetLike.instMembership Submodule.setLike Submodule.span Set.range NumberField.Units.dirichletUnitTheorem.w₀ completeFamily	Finset.sum Finset.univ NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.instZero	—	Submodule.span_induction Finset.sum_congr Subtype.prop NumberField.to_charZero sum_expMap_symm_apply NumberField.Units.coe_ne_zero NumberField.Units.norm Rat.cast_one Real.log_one Finset.sum_const_zero Finset.sum_add_distrib add_zero MulZeroClass.mul_zero
sum_expMap_symm_apply 📖	mathematical	—	Finset.sum NumberField.InfinitePlace Real Real.instAddCommMonoid Finset.univ NumberField.InfinitePlace.NumberField.InfinitePlace.fintype OpenPartialHomeomorph.toFun' NumberField.mixedEmbedding.realSpace Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm expMap NumberField.mixedEmbedding.normAtAllPlaces DFunLike.coe RingHom NumberField.mixedEmbedding.mixedSpace Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace.IsReal Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding Real.log Real.instRatCast abs Rat.instLattice Rat.addGroup MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring Rat.commRing MonoidHom.instFunLike Algebra.norm DivisionRing.toRatAlgebra NumberField.to_charZero	—	NumberField.to_charZero Real.log_prod pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass map_ne_zero Real.instNontrivial NumberField.InfinitePlace.instMonoidWithZeroHomClassReal Finset.sum_congr Real.log_pow NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding
volume_frontier_normLeOne 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure NumberField.mixedEmbedding.mixedSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex Complex measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume frontier instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField normLeOne instZeroENNReal	—	Complex.instFiniteDimensionalReal Complex.borelSpace frontier.eq_1 MeasureTheory.measure_diff interior_subset_closure MeasurableSet.nullMeasurableSet measurableSet_interior Prod.opensMeasurableSpace Pi.opensMeasurableSpace Subtype.countable Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace secondCountable_of_proper Complex.instProperSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable lt_top_iff_ne_top lt_of_le_of_lt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass interior_subset Nat.instAtLeastTwoHAddOfNat volume_normLeOne volume_interior_eq_volume_closure tsub_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub
volume_interior_eq_volume_closure 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure NumberField.mixedEmbedding.mixedSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex Complex measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume interior instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField normLeOne closure	—	MeasurableSet.preimage IsCompact.measurableSet Pi.opensMeasurableSpace Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace isCompact_compactSet Continuous.measurable Prod.opensMeasurableSpace Subtype.countable secondCountable_of_proper Complex.instProperSpace Complex.borelSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable Pi.borelSpace NumberField.mixedEmbedding.continuous_normAtAllPlaces MeasurableSet.image_of_continuousOn_injOn instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.instSeparableSpaceForallOfCountable TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.IsCompletelyMetrizableSpace.pi_countable TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace measurableSet_interior Continuous.continuousOn continuous_expMapBasis Function.Injective.injOn injective_expMapBasis le_antisymm Complex.instFiniteDimensionalReal MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass interior_subset_closure LE.le.trans closure_normLeOne_subset Nat.instAtLeastTwoHAddOfNat NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage NumberField.mixedEmbedding.normAtAllPlaces_image_preimage_of_nonneg nonneg_of_mem_compactSet normAtAllPlaces_image_preimage_expMapBasis MeasureTheory.setLIntegral_congr compactSet_ae NumberField.to_charZero setLIntegral_expMapBasis_image measurableSet_closure Finset.measurable_prod ENNReal.instMeasurableMul₂ Measurable.ennreal_ofReal measurable_pi_apply closure_paramSet_ae_interior subset_interior_normLeOne
volume_normLeOne 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure NumberField.mixedEmbedding.mixedSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex Complex measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume normLeOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat NumberField.InfinitePlace.nrRealPlaces ENNReal.ofNNReal NNReal.pi NumberField.InfinitePlace.nrComplexPlaces ENNReal.ofReal NumberField.Units.regulator	—	Complex.instFiniteDimensionalReal Complex.borelSpace Nat.instAtLeastTwoHAddOfNat NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral normLeOne_eq_preimage_image measurableSet_normLeOne normLeOne_eq_preimage normAtAllPlaces_image_preimage_expMapBasis NumberField.to_charZero setLIntegral_expMapBasis_image measurableSet_paramSet Finset.measurable_prod ENNReal.instMeasurableMul₂ Measurable.ennreal_ofReal measurable_pi_apply ENNReal.inv_mul_cancel_right Finset.prod_ne_zero_iff ENNReal.instNoZeroDivisors ENNReal.ofReal_ne_zero_iff expMapBasis_pos ENNReal.prod_ne_top ENNReal.ofReal_ne_top setLIntegral_paramSet_exp Module.finrank_pos commRing_strongRankCondition Rat.nontrivial NumberField.to_finiteDimensional Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing ENNReal.ofReal_mul zero_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_pow ENNReal.ofReal_ofNat ENNReal.mul_inv_cancel_right Nat.cast_ne_zero ENNReal.instCharZero LT.lt.ne' ENNReal.natCast_ne_top ENNReal.coe_nnreal_eq NNReal.coe_real_pi mul_mul_mul_comm ENNReal.inv_pow mul_assoc pow_ne_zero isReduced_of_noZeroDivisors two_ne_zero ZeroLEOneClass.neZero.two IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instIsOrderedAddMonoid ENNReal.pow_ne_top ENNReal.ofNat_ne_top
zero_mem_compactSet 📖	mathematical	—	NumberField.mixedEmbedding.realSpace Set Set.instMembership compactSet Pi.instZero NumberField.InfinitePlace Real Real.instZero	—	Set.zero_mem_smul_iff Real.instIsDomain Pi.instModuleIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Set.left_mem_Icc zero_le_one Real.instZeroLEOneClass Set.image_nonempty Set.univ_pi_nonempty_iff

---

← Back to Index