Basic

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

Statistics

Metric	Count
Definitions canonicalEmbedding, integerLattice, latticeBasis, mixedEmbedding, commMap, instRingMixedSpace, integerLattice, mixedSpace, stdOrthonormalBasis, toMixed, fractionalIdealLatticeBasis, idealLattice, index, indexEquiv, integerLattice, latticeBasis, matrixToStdBasis, mixedSpace, mixedSpaceOfRealSpace, negAt, norm, normAtAllPlaces, normAtComplexPlaces, normAtPlace, plusPart, realSpace, signSet, stdBasis	28
Theorems apply_at, conj_apply, inter_ball_finite, integralBasis_repr_apply, latticeBasis_apply, mem_rat_span_latticeBasis, mem_span_latticeBasis, nnnorm_eq, norm_le_iff, canonicalEmbedding_injective, commMap_apply_of_isComplex, commMap_apply_of_isReal, commMap_canonical_eq_mixed, continuous_norm, continuous_normAtAllPlaces, continuous_normAtPlace, det_basisOfFractionalIdeal_eq_norm, det_matrixToStdBasis, disjoint_negAt_plusPart, disjoint_span_commMap_ker, finrank, instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, instIsZLatticeRealMixedSpaceIntegerLattice, instNontrivialMixedSpace, stdOrthonormalBasis_map_eq, volumePreserving_toMixed, volumePreserving_toMixed_symm, exists_normAtPlace_ne_zero_iff, finrank, forall_normAtPlace_eq_zero_iff, fractionalIdealLatticeBasis_apply, fundamentalDomain_idealLattice, fundamentalDomain_integerLattice, fundamentalDomain_stdBasis, iUnion_negAt_plusPart_ae, iUnion_negAt_plusPart_union, indexEquiv_apply_isComplex_fst, indexEquiv_apply_isComplex_snd, indexEquiv_apply_isReal, injective_mixedSpaceOfRealSpace, instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, instIsAddHaarMeasureMixedSpaceVolume, instIsZLatticeRealMixedSpaceIdealLattice, instIsZLatticeRealMixedSpaceIntegerLattice, instNoAtomsMixedSpaceVolume, instNontrivialMixedSpace, latticeBasis_apply, latticeBasis_repr_apply, measurableSet_negAt_plusPart, measurableSet_plusPart, mem_idealLattice, mem_negAt_plusPart_of_mem, mem_rat_span_latticeBasis, mem_span_fractionalIdealLatticeBasis, mem_span_latticeBasis, mixedEmbedding_apply_isComplex, mixedEmbedding_apply_isReal, mixedSpaceOfRealSpace_apply, negAt_apply_isComplex, negAt_apply_isReal_and_mem, negAt_apply_isReal_and_notMem, negAt_apply_norm_isReal, negAt_apply_snd, negAt_preimage, negAt_signSet_apply_isComplex, negAt_signSet_apply_isReal, negAt_symm, neg_of_mem_negA_plusPart, nnnorm_eq_sup_normAtPlace, normAtAllPlaces_apply, normAtAllPlaces_eq_of_normAtComplexPlaces_eq, normAtAllPlaces_image_preimage_of_nonneg, normAtAllPlaces_mixedEmbedding, normAtAllPlaces_mixedSpaceOfRealSpace, normAtAllPlaces_nonneg, normAtAllPlaces_normAtAllPlaces, normAtAllPlaces_norm_at_real_places, normAtComplexPlaces_apply_isComplex, normAtComplexPlaces_apply_isReal, normAtComplexPlaces_mixedSpaceOfRealSpace, normAtComplexPlaces_normAtAllPlaces, normAtPlace_add_le, normAtPlace_apply, normAtPlace_apply_of_isComplex, normAtPlace_apply_of_isReal, normAtPlace_mixedSpaceOfRealSpace, normAtPlace_neg, normAtPlace_negAt, normAtPlace_nonneg, normAtPlace_real, normAtPlace_smul, norm_apply, norm_eq_norm, norm_eq_of_normAtPlace_eq, norm_eq_sup'_normAtPlace, norm_eq_zero_iff, norm_eq_zero_iff', norm_ne_zero_iff, norm_negAt, norm_nonneg, norm_real, norm_smul, norm_unit, pos_of_notMem_negAt_plusPart, volume_eq_zero, span_idealLatticeBasis, span_latticeBasis, stdBasis_apply_isComplex_fst, stdBasis_apply_isComplex_snd, stdBasis_apply_isReal, stdBasis_repr_eq_matrixToStdBasis_mul, volume_eq_two_pow_mul_volume_plusPart, volume_eq_zero, volume_fundamentalDomain_stdBasis, volume_negAt_plusPart, volume_preserving_negAt, mixedEmbedding_injective	118
Total	146

NumberField

Definitions

Name	Category	Theorems
canonicalEmbedding 📖	CompOp	11 math math: canonicalEmbedding.mem_span_latticeBasis, canonicalEmbedding.latticeBasis_apply, canonicalEmbedding.integralBasis_repr_apply, canonicalEmbedding.nnnorm_eq, inverse_basisMatrix_mulVec_eq_repr, canonicalEmbedding.mem_rat_span_latticeBasis, canonicalEmbedding.norm_le_iff, canonicalEmbedding_injective, canonicalEmbedding.apply_at, canonicalEmbedding_eq_basisMatrix_mulVec, mixedEmbedding.commMap_canonical_eq_mixed
mixedEmbedding 📖	CompOp	30 math math: mixedEmbedding.convexBodyLT'_mem, mixedEmbedding.norm_eq_norm, mixedEmbedding.mem_idealLattice, mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, mixedEmbedding.convexBodyLT_mem, InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, mixedEmbedding.mem_span_fractionalIdealLatticeBasis, mixedEmbedding.unit_smul_eq_iff_mul_eq, mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet, mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, mixedEmbedding.logMap_eq_logEmbedding, mixedEmbedding.mixedEmbedding_apply_isReal, mixedEmbedding.normAtAllPlaces_mixedEmbedding, mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, mixedEmbedding.unitSMul_smul, mixedEmbedding.normAtPlace_apply, mixedEmbedding_injective, mixedEmbedding.latticeBasis_apply, mixedEmbedding.latticeBasis_repr_apply, mixedEmbedding.fractionalIdealLatticeBasis_apply, mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, mixedEmbedding.fundamentalCone.mem_idealSet, mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, mixedEmbedding.mixedEmbedding_apply_isComplex, mixedEmbedding.fundamentalCone.mem_integerSet, mixedEmbedding.commMap_canonical_eq_mixed, mixedEmbedding.norm_unit, mixedEmbedding.fundamentalCone.expMap_basis_of_ne, mixedEmbedding.convexBodySum_mem, mixedEmbedding.mem_rat_span_latticeBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canonicalEmbedding_injective 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Pi.nonAssocSemiring Complex Complex.instSemiring RingHom.instFunLike canonicalEmbedding	—	RingHom.injective DivisionRing.isSimpleRing Function.nontrivial Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed Complex.instNontrivial
mixedEmbedding_injective 📖	mathematical	—	mixedEmbedding.mixedSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring InfinitePlace InfinitePlace.IsReal Real Real.semiring InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike mixedEmbedding	—	RingHom.injective DivisionRing.isSimpleRing mixedEmbedding.instNontrivialMixedSpace

NumberField.canonicalEmbedding

Definitions

Name	Category	Theorems
integerLattice 📖	CompOp	1 math math: integerLattice.inter_ball_finite
latticeBasis 📖	CompOp	5 math math: mem_span_latticeBasis, latticeBasis_apply, integralBasis_repr_apply, mem_rat_span_latticeBasis, NumberField.mixedEmbedding.disjoint_span_commMap_ker

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_at 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Pi.nonAssocSemiring Complex Complex.instSemiring RingHom.instFunLike NumberField.canonicalEmbedding	—	—
conj_apply 📖	mathematical	Submodule Real Real.semiring Pi.addCommMonoid RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Pi.nonAssocSemiring RingHom.instFunLike NumberField.canonicalEmbedding	CommSemiring.toSemiring Complex.instCommSemiring starRingEnd Complex.instStarRing NumberField.ComplexEmbedding.conjugate	—	Submodule.span_induction apply_at NumberField.ComplexEmbedding.conjugate_coe_eq Pi.zero_apply map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Pi.add_apply map_add SemilinearMapClass.toAddHomClass Complex.instCharZero RingHomClass.toLinearMapClassNNRat Pi.smul_apply Complex.real_smul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Complex.conj_ofReal
integralBasis_repr_apply 📖	mathematical	—	DFunLike.coe Finsupp Module.Free.ChooseBasisIndex NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt Complex MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Complex.instSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Pi.addCommMonoid RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finsupp.instAddCommMonoid Pi.Function.module Complex.instModuleSelf Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr latticeBasis Pi.nonAssocSemiring RingHom.instFunLike NumberField.canonicalEmbedding Complex.instRatCast Rat.semiring EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero NumberField.integralBasis	—	NumberField.RingOfIntegers.instFreeInt RingHomInvPair.ids NumberField.to_charZero Complex.instCharZero Rat.isDomain Complex.instNontrivial IsScalarTower.rat instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors mem_rat_span_latticeBasis Module.Basis.restrictScalars_repr_apply eq_ratCast RingHom.instRingHomClass RingHomCompTriple.ids Module.Basis.ext Subtype.val_injective LinearMap.codRestrict_apply AlgHom.toLinearMap_apply Module.Basis.restrictScalars_apply latticeBasis_apply Module.Basis.repr_self DFunLike.congr_fun LinearMap.congr_fun
latticeBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis Module.Free.ChooseBasisIndex NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt Complex Complex.instSemiring Pi.addCommMonoid RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module Complex.instModuleSelf Module.Basis.instFunLike latticeBasis Pi.nonAssocSemiring RingHom.instFunLike NumberField.canonicalEmbedding Rat.semiring EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero NumberField.integralBasis	—	NumberField.RingOfIntegers.instFreeInt NumberField.to_charZero Complex.instCharZero NumberField.integralBasis_apply basisOfPiSpaceOfLinearIndependent.congr_simp Module.Basis.coe_reindex coe_basisOfPiSpaceOfLinearIndependent Equiv.apply_symm_apply
mem_rat_span_latticeBasis 📖	mathematical	—	Submodule Rat.semiring Pi.addCommMonoid RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module NormedSpace.toModule Rat.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace normedAlgebraRat NormedField.toNormedDivisionRing Complex.instCharZero RCLike.toNormedAlgebra Complex.instRCLike SetLike.instMembership Submodule.setLike Submodule.span Set.range Module.Free.ChooseBasisIndex NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt DFunLike.coe Module.Basis Complex.instModuleSelf Module.Basis.instFunLike latticeBasis Pi.nonAssocSemiring RingHom.instFunLike NumberField.canonicalEmbedding	—	Complex.instCharZero NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt NumberField.to_charZero RingHomInvPair.ids Module.Basis.sum_repr map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr map_rat_smul Submodule.sum_smul_mem Submodule.subset_span latticeBasis_apply Set.mem_range_self
mem_span_latticeBasis 📖	mathematical	—	Submodule Int.instSemiring Pi.addCommMonoid RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Pi.addCommGroup Complex.addCommGroup SetLike.instMembership Submodule.setLike Submodule.span Set.range Module.Free.ChooseBasisIndex NumberField.RingOfIntegers NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt DFunLike.coe Module.Basis Pi.Function.module Complex.instModuleSelf Module.Basis.instFunLike latticeBasis Subring Pi.ring Complex.instRing Subring.instSetLike RingHom.range RingHom.comp CommSemiring.toSemiring CommRing.toCommSemiring Pi.nonAssocSemiring NumberField.canonicalEmbedding algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring	—	NumberField.RingOfIntegers.instFreeInt NumberField.to_charZero Set.range_comp latticeBasis_apply RingHomSurjective.ids Submodule.map_span SetLike.mem_coe Submodule.map_coe RingHom.map_range Subring.mem_map Set.mem_image NumberField.mem_span_integralBasis
nnnorm_eq 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm Pi.seminormedAddGroup RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring NumberField.Embeddings.instFintypeRingHom Complex.instField Complex.instCharZero SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField DFunLike.coe Pi.nonAssocSemiring RingHom.instFunLike NumberField.canonicalEmbedding Finset.sup NNReal instSemilatticeSupNNReal NNReal.instOrderBot Finset.univ	—	Complex.instCharZero Pi.nnnorm_def
norm_le_iff 📖	mathematical	—	Real Real.instLE Norm.norm NormedRing.toNorm Pi.normedRing RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring NumberField.Embeddings.instFintypeRingHom Complex.instField Complex.instCharZero NormedCommRing.toNormedRing NormedField.toNormedCommRing Complex.instNormedField DFunLike.coe Pi.nonAssocSemiring RingHom.instFunLike NumberField.canonicalEmbedding Complex.instNorm	—	Complex.instCharZero lt_or_ge NumberField.Embeddings.instNonemptyRingHom Complex.isAlgClosed LT.lt.not_ge LT.lt.trans_le norm_nonneg le_trans CanLift.prf NNReal.canLift nnnorm_eq

NumberField.canonicalEmbedding.integerLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_ball_finite 📖	mathematical	—	Set.Finite Set Set.instInter SetLike.coe Subring Pi.ring RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring Complex.instRing Subring.instSetLike NumberField.canonicalEmbedding.integerLattice Metric.closedBall pseudoMetricSpacePi NumberField.Embeddings.instFintypeRingHom Complex.instField Complex.instCharZero SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Pi.instZero Complex.instZero	—	Complex.instCharZero lt_or_ge Metric.closedBall_eq_empty Set.inter_empty NumberField.canonicalEmbedding.norm_le_iff mem_closedBall_zero_iff Set.ext SetLike.coe_mem Set.Finite.image NumberField.Embeddings.finite_of_norm_le Complex.isAlgClosed

NumberField.mixedEmbedding

Definitions

Name	Category	Theorems
commMap 📖	CompOp	5 math math: commMap_apply_of_isComplex, stdBasis_repr_eq_matrixToStdBasis_mul, commMap_apply_of_isReal, disjoint_span_commMap_ker, commMap_canonical_eq_mixed
fractionalIdealLatticeBasis 📖	CompOp	5 math math: fundamentalDomain_idealLattice, mem_span_fractionalIdealLatticeBasis, span_idealLatticeBasis, volume_fundamentalDomain_fractionalIdealLatticeBasis, fractionalIdealLatticeBasis_apply
idealLattice 📖	CompOp	6 math math: mem_idealLattice, fundamentalDomain_idealLattice, instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, span_idealLatticeBasis, covolume_idealLattice, instIsZLatticeRealMixedSpaceIdealLattice
index 📖	CompOp	11 math math: stdBasis_apply_isComplex_snd, euclidean.stdOrthonormalBasis_map_eq, indexEquiv_apply_isComplex_fst, stdBasis_apply_isComplex_fst, fundamentalDomain_stdBasis, stdBasis_repr_eq_matrixToStdBasis_mul, det_matrixToStdBasis, indexEquiv_apply_isReal, stdBasis_apply_isReal, indexEquiv_apply_isComplex_snd, volume_fundamentalDomain_stdBasis
indexEquiv 📖	CompOp	4 math math: indexEquiv_apply_isComplex_fst, stdBasis_repr_eq_matrixToStdBasis_mul, indexEquiv_apply_isReal, indexEquiv_apply_isComplex_snd
integerLattice 📖	CompOp	6 math math: fundamentalDomain_integerLattice, mem_span_latticeBasis, span_latticeBasis, covolume_integerLattice, instIsZLatticeRealMixedSpaceIntegerLattice, instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice
latticeBasis 📖	CompOp	9 math math: fundamentalDomain_integerLattice, mem_span_latticeBasis, det_basisOfFractionalIdeal_eq_norm, span_latticeBasis, volume_fundamentalDomain_fractionalIdealLatticeBasis, latticeBasis_apply, latticeBasis_repr_apply, volume_fundamentalDomain_latticeBasis, mem_rat_span_latticeBasis
matrixToStdBasis 📖	CompOp	2 math math: stdBasis_repr_eq_matrixToStdBasis_mul, det_matrixToStdBasis
mixedSpace 📖	CompOp	184 math math: integral_comp_polarSpaceCoord_symm, fundamentalDomain_integerLattice, normAtComplexPlaces_mixedSpaceOfRealSpace, logMap_one, lintegral_comp_polarCoord_symm, norm_eq_sup'_normAtPlace, convexBodyLT'_mem, convexBodySumFun_add_le, normAtAllPlaces_apply, fundamentalCone.integerSetEquivNorm_apply_fst, normAtPlace_polarCoord_symm_of_isComplex, norm_unit_smul, norm_eq_norm, norm_le_convexBodySumFun, mem_idealLattice, fundamentalCone.completeBasis_apply_of_ne, instIsAddHaarMeasureMixedSpaceVolume, commMap_apply_of_isComplex, instNoAtomsMixedSpaceVolume, fundamentalCone.card_isPrincipal_dvd_norm_le, convexBodyLT_volume, instNontrivialMixedSpace, polarSpaceCoord_target, negAt_apply_snd, convexBodyLT_mem, fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, negAt_preimage, fundamentalCone.volume_frontier_normLeOne, normAtPlace_apply_of_isReal, fundamentalCone.integerSetQuotEquivAssociates_apply, stdBasis_apply_isComplex_snd, negAt_signSet_apply_isComplex, fundamentalCone.volume_interior_eq_volume_closure, euclidean.stdOrthonormalBasis_map_eq, convexBodySum_volume_eq_zero_of_le_zero, normAtComplexPlaces_polarSpaceCoord_symm, fundamentalCone.logMap_expMapBasis, fundamentalCone.integerSetEquiv_apply_fst, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, convexBodySum_compact, fundamentalCone.subset_interior_normLeOne, negAt_signSet_apply_isReal, fundamentalDomain_idealLattice, fundamentalCone.integerSetTorsionSMul_smul_coe, mem_span_fractionalIdealLatticeBasis, instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, convexBodySumFun_apply, fundamentalCone.mem_normLeOne, span_idealLatticeBasis, fundamentalCone.norm_expMapBasis, convexBodySumFun_smul, logMap_real_smul, polarCoord_symm_apply, unit_smul_eq_iff_mul_eq, fundamentalCone.integerSetTorsionSMul_stabilizer, mem_span_latticeBasis, euclidean.volumePreserving_toMixed, negAt_apply_isReal_and_notMem, covolume_idealLattice, volume_preserving_negAt, normAtPlace_add_le, negAt_apply_isComplex, fundamentalCone.normLeOne_eq_preimage_image, normAtComplexPlaces_normAtAllPlaces, fundamentalCone.quotIntNorm_apply, fundamentalCone.idealSetMap_apply, fundamentalCone.exists_unit_smul_mem, fundamentalCone.closure_normLeOne_subset, convexBodySumFun_neg, convexBodySumFun_continuous, det_basisOfFractionalIdeal_eq_norm, logMap_eq_logEmbedding, fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, volume_preserving_mixedSpaceToRealMixedSpace_symm, norm_nonneg, mixedEmbedding_apply_isReal, stdBasis_apply_isComplex_fst, norm_smul, fundamentalDomain_stdBasis, span_latticeBasis, measurableSet_fundamentalCone, polarCoord_source, stdBasis_repr_eq_matrixToStdBasis_mul, continuous_norm, polarSpaceCoord_symm_apply, fundamentalCone.norm_normAtAllPlaces, normAtAllPlaces_mixedEmbedding, covolume_integerLattice, mixedSpaceToRealMixedSpace_apply, polarCoord_target, normAtPlace_polarCoord_symm_of_isReal, negAt_symm, fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, polarCoord_symm_eq, volume_fundamentalDomain_fractionalIdealLatticeBasis, instIsZLatticeRealMixedSpaceIntegerLattice, negAt_apply_isReal_and_mem, polarSpaceCoord_target', convexBodyLT'_volume, fundamentalCone.integerSetToAssociates_eq_iff, logMap_unit_smul, normAtPlace_neg, unitSMul_smul, continuous_normAtPlace, injective_mixedSpaceOfRealSpace, normAtPlace_apply, volume_eq_zero, stdBasis_apply_isReal, instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, normAtPlace_apply_of_isComplex, NumberField.mixedEmbedding_injective, forall_normAtPlace_eq_zero_iff, convexBodyLT_convex, instIsZLatticeRealMixedSpaceIdealLattice, fundamentalCone.idealSetEquiv_symm_apply, logMap_apply, latticeBasis_apply, unit_smul_eq_zero, measurable_polarCoord_symm, fundamentalCone.intNorm_coe, norm_eq_zero_iff, normAtPlace_nonneg, logMap_real, commMap_apply_of_isReal, polarCoord_apply, continuous_normAtAllPlaces, latticeBasis_repr_apply, normAtPlace_negAt, normAtPlace_smul, fundamentalCone.isBounded_normLeOne, finrank, fractionalIdealLatticeBasis_apply, convexBodySum_isBounded, polarSpaceCoord_apply, normAtAllPlaces_image_preimage_of_nonneg, negAt_apply_norm_isReal, norm_real, volume_fundamentalDomain_latticeBasis, polarSpaceCoord_source, logMap_torsion_smul, polarCoord_target_eq_polarCoordReal_target, fundamentalCone.realSpaceToLogSpace_expMap_symm, euclidean.volumePreserving_toMixed_symm, convexBodySum_convex, fundamentalCone.mem_idealSet, fundamentalCone.volume_normLeOne, fundamentalCone.integerSetToAssociates_surjective, fundamentalCone.idealSetEquiv_apply, fundamentalCone.sum_expMap_symm_apply, fundamentalCone.normAtAllPlaces_image_preimage_expMapBasis, mixedEmbedding_apply_isComplex, fundamentalCone.smul_mem_iff_mem, fundamentalCone.mem_integerSet, normAtAllPlaces_mixedSpaceOfRealSpace, fundamentalCone.normAtAllPlaces_normLeOne_eq_image, disjoint_span_commMap_ker, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, convexBodySum_volume, logMap_zero, integral_comp_polarCoord_symm, fundamentalCone.measurableSet_normLeOne, commMap_canonical_eq_mixed, norm_negAt, norm_unit, fundamentalCone.normLeOne_eq_preimage, normAtPlace_mixedSpaceOfRealSpace, measurable_polarSpaceCoord_symm, nnnorm_eq_sup_normAtPlace, fundamentalCone.expMap_basis_of_ne, disjoint_negAt_plusPart, logMap_mul, volume_fundamentalDomain_stdBasis, convexBodySum_mem, convexBodyLT'_convex, mem_rat_span_latticeBasis, norm_apply, fundamentalCone.logMap_normAtAllPlaces, fundamentalCone.normAtAllPlaces_normLeOne, normAtAllPlaces_normAtAllPlaces, normAtPlace_real, fundamentalCone.intNorm_idealSetEquiv_apply, mixedSpaceOfRealSpace_apply, convexBodySumFun_eq_zero_iff, lintegral_comp_polarSpaceCoord_symm
mixedSpaceOfRealSpace 📖	CompOp	14 math math: normAtComplexPlaces_mixedSpaceOfRealSpace, normAtComplexPlaces_polarSpaceCoord_symm, fundamentalCone.logMap_expMapBasis, fundamentalCone.norm_expMapBasis, normAtComplexPlaces_normAtAllPlaces, fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, fundamentalCone.norm_normAtAllPlaces, injective_mixedSpaceOfRealSpace, normAtAllPlaces_mixedSpaceOfRealSpace, normAtPlace_mixedSpaceOfRealSpace, fundamentalCone.logMap_normAtAllPlaces, fundamentalCone.normAtAllPlaces_normLeOne, normAtAllPlaces_normAtAllPlaces, mixedSpaceOfRealSpace_apply
negAt 📖	CompOp	18 math math: negAt_apply_snd, negAt_preimage, iUnion_negAt_plusPart_ae, negAt_signSet_apply_isComplex, negAt_signSet_apply_isReal, negAt_apply_isReal_and_notMem, volume_preserving_negAt, negAt_apply_isComplex, mem_negAt_plusPart_of_mem, negAt_symm, negAt_apply_isReal_and_mem, volume_negAt_plusPart, iUnion_negAt_plusPart_union, normAtPlace_negAt, negAt_apply_norm_isReal, measurableSet_negAt_plusPart, norm_negAt, disjoint_negAt_plusPart
norm 📖	CompOp	23 math math: norm_eq_zero_iff', fundamentalCone.integerSetEquivNorm_apply_fst, norm_unit_smul, norm_eq_norm, fundamentalCone.card_isPrincipal_dvd_norm_le, fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, fundamentalCone.norm_pos_of_mem, fundamentalCone.mem_normLeOne, fundamentalCone.norm_expMapBasis, norm_nonneg, norm_smul, continuous_norm, fundamentalCone.norm_normAtAllPlaces, logMap_apply, fundamentalCone.intNorm_coe, norm_eq_zero_iff, norm_eq_of_normAtPlace_eq, norm_real, norm_negAt, norm_unit, norm_apply, fundamentalCone.normAtAllPlaces_normLeOne, fundamentalCone.intNorm_idealSetEquiv_apply
normAtAllPlaces 📖	CompOp	24 math math: normAtAllPlaces_apply, fundamentalCone.completeBasis_apply_of_ne, fundamentalCone.subset_interior_normLeOne, fundamentalCone.normLeOne_eq_preimage_image, normAtComplexPlaces_normAtAllPlaces, fundamentalCone.closure_normLeOne_subset, fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, fundamentalCone.norm_normAtAllPlaces, normAtAllPlaces_mixedEmbedding, normAtAllPlaces_eq_of_normAtComplexPlaces_eq, continuous_normAtAllPlaces, normAtAllPlaces_nonneg, normAtAllPlaces_image_preimage_of_nonneg, normAtAllPlaces_norm_at_real_places, fundamentalCone.realSpaceToLogSpace_expMap_symm, fundamentalCone.sum_expMap_symm_apply, fundamentalCone.normAtAllPlaces_image_preimage_expMapBasis, normAtAllPlaces_mixedSpaceOfRealSpace, fundamentalCone.normAtAllPlaces_normLeOne_eq_image, fundamentalCone.normLeOne_eq_preimage, fundamentalCone.expMap_basis_of_ne, fundamentalCone.logMap_normAtAllPlaces, fundamentalCone.normAtAllPlaces_normLeOne, normAtAllPlaces_normAtAllPlaces
normAtComplexPlaces 📖	CompOp	5 math math: normAtComplexPlaces_mixedSpaceOfRealSpace, normAtComplexPlaces_polarSpaceCoord_symm, normAtComplexPlaces_normAtAllPlaces, normAtComplexPlaces_apply_isComplex, normAtComplexPlaces_apply_isReal
normAtPlace 📖	CompOp	24 math math: norm_eq_sup'_normAtPlace, normAtAllPlaces_apply, normAtPlace_polarCoord_symm_of_isComplex, normAtPlace_apply_of_isReal, convexBodySumFun_apply, normAtPlace_add_le, logMap_apply_of_norm_eq_one, normAtPlace_polarCoord_symm_of_isReal, fundamentalCone.normAtPlace_pos_of_mem, normAtPlace_neg, continuous_normAtPlace, normAtPlace_apply, normAtPlace_apply_of_isComplex, forall_normAtPlace_eq_zero_iff, logMap_apply, norm_eq_zero_iff, logMap_apply_of_norm_one, normAtPlace_nonneg, normAtPlace_negAt, normAtPlace_smul, normAtPlace_mixedSpaceOfRealSpace, nnnorm_eq_sup_normAtPlace, norm_apply, normAtPlace_real
plusPart 📖	CompOp	8 math math: measurableSet_plusPart, iUnion_negAt_plusPart_ae, mem_negAt_plusPart_of_mem, volume_negAt_plusPart, iUnion_negAt_plusPart_union, measurableSet_negAt_plusPart, disjoint_negAt_plusPart, volume_eq_two_pow_mul_volume_plusPart
realSpace 📖	CompOp	67 math math: fundamentalCone.expMapBasis_apply', normAtComplexPlaces_mixedSpaceOfRealSpace, fundamentalCone.interior_paramSet, fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, fundamentalCone.abs_det_completeBasis_equivFunL_symm, fundamentalCone.completeBasis_apply_of_ne, fundamentalCone.expMap_target, fundamentalCone.isCompact_compactSet, normAtComplexPlaces_polarSpaceCoord_symm, fundamentalCone.logMap_expMapBasis, fundamentalCone.subset_interior_normLeOne, fundamentalCone.realSpaceToLogSpace_completeFamily_of_eq, fundamentalCone.prod_deriv_expMap_single, fundamentalCone.norm_expMapBasis, fundamentalCone.completeBasis_apply_of_eq, realSpace.volume_eq_zero, fundamentalCone.expMap_basis_of_eq, fundamentalCone.prod_expMapBasis_pow, fundamentalCone.normLeOne_eq_preimage_image, fundamentalCone.expMapBasis_closure_subset_compactSet, fundamentalCone.continuous_expMap, normAtComplexPlaces_normAtAllPlaces, fundamentalCone.expMap_smul, fundamentalCone.realSpaceToLogSpace_apply, fundamentalCone.closure_normLeOne_subset, fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, fundamentalCone.hasFDerivAt_expMap, fundamentalCone.continuous_expMapBasis, fundamentalCone.expMap_symm_apply, fundamentalCone.norm_normAtAllPlaces, fundamentalCone.closure_paramSet, fundamentalCone.hasFDerivAt_expMapBasis, fundamentalCone.setLIntegral_paramSet_exp, injective_mixedSpaceOfRealSpace, fundamentalCone.expMapBasis_pos, fundamentalCone.expMap_apply, fundamentalCone.injective_expMapBasis, fundamentalCone.expMap_source, fundamentalCone.expMapBasis_apply'', continuous_normAtAllPlaces, normAtAllPlaces_image_preimage_of_nonneg, fundamentalCone.expMap_add, fundamentalCone.expMapBasis_apply, fundamentalCone.compactSet_ae, fundamentalCone.abs_det_fderiv_expMapBasis, fundamentalCone.realSpaceToLogSpace_expMap_symm, fundamentalCone.zero_mem_compactSet, fundamentalCone.sum_expMap_symm_apply, fundamentalCone.normAtAllPlaces_image_preimage_expMapBasis, normAtAllPlaces_mixedSpaceOfRealSpace, fundamentalCone.expMap_sum, fundamentalCone.normAtAllPlaces_normLeOne_eq_image, fundamentalCone.expMapBasis_source, fundamentalCone.measurableSet_paramSet, fundamentalCone.expMap_pos, fundamentalCone.linearIndependent_completeFamily, fundamentalCone.normLeOne_eq_preimage, fundamentalCone.compactSet_eq_union, normAtPlace_mixedSpaceOfRealSpace, fundamentalCone.injective_expMap, fundamentalCone.expMap_basis_of_ne, fundamentalCone.expMapBasis_nonneg, fundamentalCone.logMap_normAtAllPlaces, fundamentalCone.normAtAllPlaces_normLeOne, normAtAllPlaces_normAtAllPlaces, mixedSpaceOfRealSpace_apply, fundamentalCone.closure_paramSet_ae_interior
signSet 📖	CompOp	2 math math: negAt_signSet_apply_isComplex, negAt_signSet_apply_isReal
stdBasis 📖	CompOp	7 math math: stdBasis_apply_isComplex_snd, euclidean.stdOrthonormalBasis_map_eq, stdBasis_apply_isComplex_fst, fundamentalDomain_stdBasis, stdBasis_repr_eq_matrixToStdBasis_mul, stdBasis_apply_isReal, volume_fundamentalDomain_stdBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commMap_apply_of_isComplex 📖	mathematical	NumberField.InfinitePlace.IsComplex	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring mixedSpace Pi.addCommMonoid RingHom Complex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instAddCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex Prod.instModule Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike commMap NumberField.InfinitePlace.embedding	—	—
commMap_apply_of_isReal 📖	mathematical	NumberField.InfinitePlace.IsReal	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring mixedSpace Pi.addCommMonoid RingHom Complex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instAddCommMonoid NumberField.InfinitePlace Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex Prod.instModule Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike commMap Complex.re NumberField.InfinitePlace.embedding	—	—
commMap_canonical_eq_mixed 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring mixedSpace Pi.addCommMonoid RingHom Complex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instAddCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex Prod.instModule Real.normedCommRing RCLike.toInnerProductSpaceReal LinearMap.instFunLike commMap Pi.nonAssocSemiring RingHom.instFunLike NumberField.canonicalEmbedding Prod.instNonAssocSemiring NumberField.mixedEmbedding	—	—
continuous_norm 📖	mathematical	—	Continuous mixedSpace Real instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField DFunLike.coe MonoidWithZeroHom Prod.instMulZeroOneClass Pi.mulZeroOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring Complex.instSemiring MonoidWithZeroHom.funLike norm	—	continuous_finset_prod IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal dite_pow Continuous.comp' Continuous.pow continuous_id' Continuous.norm continuous_apply Continuous.fst Continuous.snd
continuous_normAtAllPlaces 📖	mathematical	—	Continuous mixedSpace realSpace 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 normAtAllPlaces	—	continuous_pi continuous_normAtPlace
continuous_normAtPlace 📖	mathematical	—	Continuous mixedSpace Real instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField DFunLike.coe MonoidWithZeroHom Prod.instMulZeroOneClass Pi.mulZeroOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace	—	Continuous.norm Continuous.comp' continuous_apply Continuous.fst continuous_id' Continuous.snd
det_basisOfFractionalIdeal_eq_norm 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing mixedSpace AddCommGroup.toAddCommMonoid Prod.instAddCommGroup Pi.addCommGroup NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommGroup NumberField.InfinitePlace.IsComplex Complex Complex.addCommGroup Prod.instModule Real.semiring Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField 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 instInnerProductSpaceRealComplex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Module.Free.ChooseBasisIndex NumberField.RingOfIntegers Int.instSemiring NumberField.RingOfIntegers.instCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt AlternatingMap.instFunLike Module.Basis.det Module.Free.instDecidableEqChooseBasisIndex Module.Free.ChooseBasisIndex.fintype Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt latticeBasis RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding Submodule EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring SetLike.instMembership Submodule.setLike FractionalIdeal.coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero Units.val FractionalIdeal MonoidWithZero.toMonoid FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Submodule.addCommMonoid Submodule.addCommGroup NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Module.Basis Rat.semiring Rat.commSemiring DivisionRing.toRatAlgebra NumberField.to_charZero Module.Basis.instFunLike NumberField.basisOfFractionalIdeal Equiv EquivLike.toFunLike Equiv.instEquivLike Real.instRatCast MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass FractionalIdeal.commSemiring MonoidWithZeroHom.funLike FractionalIdeal.absNorm	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt NumberField.to_charZero RCLike.charZero_rclike Module.Basis.det_apply RingHom.map_det Matrix.ext RingHomInvPair.ids latticeBasis_repr_apply eq_ratCast RingHom.instRingHomClass Rat.cast_abs Real.instIsStrictOrderedRing Equiv.symm_symm Module.Basis.coe_reindex NumberField.det_basisOfFractionalIdeal_eq_absNorm
det_matrixToStdBasis 📖	mathematical	—	Matrix.det index NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex instFintypeSum Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype instFintypeProd Fin.fintype Complex Complex.commRing matrixToStdBasis Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instMul Complex.instInv instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.I NumberField.InfinitePlace.nrComplexPlaces	—	Nat.instAtLeastTwoHAddOfNat matrixToStdBasis.eq_1 Matrix.det_fromBlocks_zero₂₁ Matrix.det_diagonal Finset.prod_const_one one_mul Matrix.det_reindex_self Matrix.det_blockDiagonal Finset.prod_congr Matrix.det.congr_simp Matrix.smul_cons mul_one Matrix.smul_empty mul_neg Matrix.det_fin_two_of sub_neg_eq_add Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false Complex.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Finset.prod_const Fintype.card.eq_1
disjoint_negAt_plusPart 📖	mathematical	—	Pairwise Set NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Function.onFun mixedSpace Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.image DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt plusPart	—	RingHomInvPair.ids Set.disjoint_left Set.symmDiff_nonempty lt_irrefl LT.lt.trans neg_of_mem_negA_plusPart pos_of_notMem_negAt_plusPart
disjoint_span_commMap_ker 📖	mathematical	—	Disjoint Submodule Real Real.semiring Pi.addCommMonoid RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex Submodule.instPartialOrder Submodule.instOrderBot Submodule.span Set.range Module.Free.ChooseBasisIndex NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt DFunLike.coe Module.Basis Complex.instModuleSelf Module.Basis.instFunLike NumberField.canonicalEmbedding.latticeBasis LinearMap.ker mixedSpace Prod.instAddCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Prod.instModule Real.normedCommRing RCLike.toInnerProductSpaceReal RingHom.id commMap	—	NumberField.RingOfIntegers.instFreeInt LinearMap.disjoint_ker Submodule.span_mono NumberField.to_charZero NumberField.canonicalEmbedding.latticeBasis_apply Pi.zero_apply Complex.ext NumberField.InfinitePlace.embedding_mk_eq_of_isReal commMap_apply_of_isReal Complex.zero_im Complex.conj_eq_iff_im NumberField.canonicalEmbedding.conj_apply NumberField.ComplexEmbedding.isReal_iff NumberField.InfinitePlace.embedding_mk_eq commMap_apply_of_isComplex RingHom.injective DivisionRing.isSimpleRing Complex.instNontrivial map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
exists_normAtPlace_ne_zero_iff 📖	—	—	—	—	forall_normAtPlace_eq_zero_iff
finrank 📖	mathematical	—	Module.finrank Real mixedSpace Real.semiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	NumberField.to_charZero Module.finrank_prod commRing_strongRankCondition Real.instNontrivial Module.Free.function Subtype.finite Finite.of_fintype Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Real.instIsDomain FiniteDimensional.rclike_to_real instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Complex.instFiniteDimensionalReal FiniteDimensional.finiteDimensional_pi' Module.finrank_pi Module.finrank_pi_fintype Complex.finrank_real_complex Finset.sum_const Finset.card_univ NumberField.InfinitePlace.nrRealPlaces.eq_1 NumberField.InfinitePlace.nrComplexPlaces.eq_1 Complex.instCharZero NumberField.InfinitePlace.card_real_embeddings smul_eq_mul mul_comm NumberField.InfinitePlace.card_complex_embeddings NumberField.Embeddings.card Complex.isAlgClosed Fintype.card_subtype_compl Fintype.card_subtype_le
forall_normAtPlace_eq_zero_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 normAtPlace Real.instZero Prod.instZero Pi.instZero Complex.instZero	—	norm_eq_zero Subtype.prop normAtPlace_apply_of_isReal normAtPlace_apply_of_isComplex map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass
fractionalIdealLatticeBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis Module.Free.ChooseBasisIndex Submodule NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield SetLike.instMembership Submodule.setLike FractionalIdeal.coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero Units.val FractionalIdeal MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Int.instSemiring Submodule.addCommMonoid AddCommGroup.toIntModule Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Real mixedSpace Real.semiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Module.Basis.instFunLike fractionalIdealLatticeBasis RingHom Semiring.toNonAssocSemiring Prod.instNonAssocSemiring Pi.nonAssocSemiring Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding Rat.semiring Rat.commSemiring DivisionRing.toRatAlgebra NumberField.to_charZero NumberField.basisOfFractionalIdeal	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule NumberField.to_charZero NumberField.RingOfIntegers.instFreeInt Module.Basis.coe_reindex Equiv.apply_symm_apply
fundamentalDomain_idealLattice 📖	mathematical	—	MeasureTheory.IsAddFundamentalDomain mixedSpace Submodule Int.instSemiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup SetLike.instMembership Submodule.setLike idealLattice Submodule.zero Submodule.instVAddSubtypeMem AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Prod.instAddMonoid Pi.addMonoid Real.instAddMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction Prod.instAddGroup Pi.addGroup Real.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Prod.instAddTorsor Finset.instAddTorsorForall Real.instRing Complex.instRing Prod.instMeasurableSpace MeasurableSpace.pi Real.measurableSpace Complex.measurableSpace ZSpan.fundamentalDomain Module.Free.ChooseBasisIndex NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield FractionalIdeal.coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero Units.val FractionalIdeal MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Submodule.addCommMonoid Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Real.normedField Prod.normedAddCommGroup Pi.normedAddCommGroup Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup Prod.normedSpace Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex fractionalIdealLatticeBasis Real.linearOrder MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Real.measureSpace measureSpaceOfInnerProductSpace Complex.instFiniteDimensionalReal Complex.borelSpace	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Complex.instFiniteDimensionalReal Complex.borelSpace span_idealLatticeBasis ZSpan.isAddFundamentalDomain Finite.of_fintype NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Prod.opensMeasurableSpace Pi.opensMeasurableSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable
fundamentalDomain_integerLattice 📖	mathematical	—	MeasureTheory.IsAddFundamentalDomain mixedSpace Submodule Int.instSemiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup SetLike.instMembership Submodule.setLike integerLattice Submodule.zero Submodule.instVAddSubtypeMem AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Prod.instAddMonoid Pi.addMonoid Real.instAddMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction Prod.instAddGroup Pi.addGroup Real.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Prod.instAddTorsor Finset.instAddTorsorForall Real.instRing Complex.instRing Prod.instMeasurableSpace MeasurableSpace.pi Real.measurableSpace Complex.measurableSpace ZSpan.fundamentalDomain Module.Free.ChooseBasisIndex NumberField.RingOfIntegers NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt Real.normedField Prod.normedAddCommGroup Pi.normedAddCommGroup Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup Prod.normedSpace Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex latticeBasis Real.linearOrder MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Real.measureSpace measureSpaceOfInnerProductSpace Complex.instFiniteDimensionalReal Complex.borelSpace	—	NumberField.RingOfIntegers.instFreeInt Complex.instFiniteDimensionalReal Complex.borelSpace span_latticeBasis ZSpan.isAddFundamentalDomain Finite.of_fintype Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt Prod.opensMeasurableSpace Pi.opensMeasurableSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable
fundamentalDomain_stdBasis 📖	mathematical	—	ZSpan.fundamentalDomain mixedSpace index Real Real.normedField Prod.normedAddCommGroup Pi.normedAddCommGroup NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup NumberField.InfinitePlace.IsComplex Complex Complex.instNormedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal NormedField.toNormedCommRing Complex.instNormedField instInnerProductSpaceRealComplex stdBasis Real.linearOrder SProd.sprod Set Set.instSProd Set.pi Set.univ Set.Ico Real.instPreorder Real.instZero Real.instOne Set.preimage DFunLike.coe MeasurableEquiv Complex.measurableSpace MeasurableSpace.pi Real.measurableSpace EquivLike.toFunLike MeasurableEquiv.instEquivLike Complex.measurableEquivPi	—	Set.ext RingHomInvPair.ids Pi.basisFun_repr Module.Basis.repr_reindex Finsupp.mapDomain_equiv_apply Matrix.cons_val_fin_one
iUnion_negAt_plusPart_ae 📖	mathematical	mixedSpace Set Set.instMembership Norm.norm Real Real.norm	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace NumberField.InfinitePlace.IsComplex Complex measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume Set.iUnion Set.image DFunLike.coe ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt plusPart	—	Complex.instFiniteDimensionalReal Complex.borelSpace MeasureTheory.Measure.instOuterMeasureClass RingHomInvPair.ids iUnion_negAt_plusPart_union Filter.EventuallyEq.symm MeasureTheory.union_ae_eq_left_of_ae_eq_empty MeasureTheory.ae_eq_empty MeasureTheory.measure_mono_null Set.inter_subset_right MeasureTheory.measure_iUnion_null_iff Subtype.countable Finite.to_countable Finite.of_fintype volume_eq_zero
iUnion_negAt_plusPart_union 📖	mathematical	mixedSpace Set Set.instMembership Norm.norm Real Real.norm	Set.instUnion Set.iUnion NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Set.image DFunLike.coe ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt plusPart Set.instInter setOf Real.instZero	—	Set.ext RingHomInvPair.ids Set.mem_union Set.mem_inter_iff Set.mem_iUnion negAt_apply_norm_isReal exists_or_forall_not mem_negAt_plusPart_of_mem lt_of_le_of_ne LT.lt.le lt_of_not_ge
indexEquiv_apply_isComplex_fst 📖	mathematical	—	DFunLike.coe Equiv index RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring EquivLike.toFunLike Equiv.instEquivLike indexEquiv NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex NumberField.InfinitePlace.embedding	—	—
indexEquiv_apply_isComplex_snd 📖	mathematical	—	DFunLike.coe Equiv index RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring EquivLike.toFunLike Equiv.instEquivLike indexEquiv NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex NumberField.ComplexEmbedding.conjugate NumberField.InfinitePlace.embedding	—	—
indexEquiv_apply_isReal 📖	mathematical	—	DFunLike.coe Equiv index RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring EquivLike.toFunLike Equiv.instEquivLike indexEquiv NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex NumberField.InfinitePlace.embedding	—	—
injective_mixedSpaceOfRealSpace 📖	mathematical	—	realSpace mixedSpace 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 mixedSpaceOfRealSpace	—	injective_iff_map_eq_zero DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass NumberField.InfinitePlace.isReal_or_isComplex Prod.mk_eq_zero mixedSpaceOfRealSpace_apply
instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice 📖	mathematical	—	DiscreteTopology mixedSpace Submodule Int.instSemiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup SetLike.instMembership Submodule.setLike idealLattice instTopologicalSpaceSubtype instTopologicalSpaceProd Pi.topologicalSpace Real.pseudoMetricSpace	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule span_idealLatticeBasis ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite Finite.of_fintype NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule
instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice 📖	mathematical	—	DiscreteTopology mixedSpace Submodule Int.instSemiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup SetLike.instMembership Submodule.setLike integerLattice instTopologicalSpaceSubtype instTopologicalSpaceProd Pi.topologicalSpace Real.pseudoMetricSpace	—	NumberField.RingOfIntegers.instFreeInt span_latticeBasis ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite Finite.of_fintype Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt
instIsAddHaarMeasureMixedSpaceVolume 📖	mathematical	—	MeasureTheory.Measure.IsAddHaarMeasure mixedSpace Prod.instAddGroup Pi.addGroup NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddGroup NumberField.InfinitePlace.IsComplex Complex NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Complex.instNormedAddCommGroup instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace measureSpaceOfInnerProductSpace instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace MeasureTheory.MeasureSpace.volume	—	MeasureTheory.Measure.prod.instIsAddHaarMeasure Complex.instFiniteDimensionalReal Complex.borelSpace MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite ContinuousAdd.measurableAdd Real.borelSpace IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup secondCountable_of_proper Complex.instProperSpace MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.instSigmaFiniteForallVolume Pi.measurableAdd
instIsZLatticeRealMixedSpaceIdealLattice 📖	mathematical	—	IsZLattice Real Real.normedField mixedSpace Prod.normedAddCommGroup Pi.normedAddCommGroup NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup NumberField.InfinitePlace.IsComplex Complex Complex.instNormedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal NormedField.toNormedCommRing Complex.instNormedField instInnerProductSpaceRealComplex idealLattice instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule IsZLattice.congr_simp instIsZLatticeRealSpan Finite.of_fintype NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule
instIsZLatticeRealMixedSpaceIntegerLattice 📖	mathematical	—	IsZLattice Real Real.normedField mixedSpace Prod.normedAddCommGroup Pi.normedAddCommGroup NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup NumberField.InfinitePlace.IsComplex Complex Complex.instNormedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal NormedField.toNormedCommRing Complex.instNormedField instInnerProductSpaceRealComplex integerLattice instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice	—	instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice NumberField.RingOfIntegers.instFreeInt IsZLattice.congr_simp instIsZLatticeRealSpan Finite.of_fintype Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt
instNoAtomsMixedSpaceVolume 📖	mathematical	—	MeasureTheory.NoAtoms 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 MeasureTheory.MeasureSpace.volume	—	Complex.instFiniteDimensionalReal Complex.borelSpace NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed MeasureTheory.Measure.pi_noAtoms 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 MeasureTheory.Measure.prod.instNoAtoms_fst SeminormedAddCommGroup.toIsTopologicalAddGroup secondCountable_of_proper Complex.instProperSpace NumberField.InfinitePlace.not_isReal_iff_isComplex MeasureTheory.Measure.IsAddHaarMeasure.noAtoms T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace PerfectSpace.not_isolated instPerfectSpace MeasureTheory.Measure.prod.instNoAtoms_snd
instNontrivialMixedSpace 📖	mathematical	—	Nontrivial mixedSpace	—	NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed NumberField.InfinitePlace.isReal_or_isComplex nontrivial_prod_left Function.nontrivial Real.instNontrivial nontrivial_prod_right Complex.instNontrivial
latticeBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis Module.Free.ChooseBasisIndex NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt Real mixedSpace Real.semiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Module.Basis.instFunLike latticeBasis RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding Rat.semiring EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero NumberField.integralBasis	—	NumberField.RingOfIntegers.instFreeInt NumberField.to_charZero coe_basisOfLinearIndependentOfCardEqFinrank NumberField.canonicalEmbedding.latticeBasis_apply NumberField.integralBasis_apply commMap_canonical_eq_mixed
latticeBasis_repr_apply 📖	mathematical	—	DFunLike.coe Finsupp Module.Free.ChooseBasisIndex NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt Real MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Real.semiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids mixedSpace Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finsupp.instAddCommMonoid Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr latticeBasis RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding Real.instRatCast Rat.semiring EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero NumberField.integralBasis	—	NumberField.RingOfIntegers.instFreeInt RingHomInvPair.ids NumberField.to_charZero RCLike.charZero_rclike Complex.instCharZero Rat.isDomain Real.instNontrivial IsScalarTower.rat instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors mem_rat_span_latticeBasis Module.Basis.restrictScalars_repr_apply eq_ratCast RingHom.instRingHomClass RingHomCompTriple.ids Module.Basis.ext Subtype.val_injective LinearMap.codRestrict_apply AlgHom.toLinearMap_apply Module.Basis.restrictScalars_apply latticeBasis_apply Module.Basis.repr_self DFunLike.congr_fun LinearMap.congr_fun
measurableSet_negAt_plusPart 📖	mathematical	MeasurableSet mixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace	Set.image DFunLike.coe ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt plusPart	—	RingHomInvPair.ids MeasurableSet.preimage measurableSet_plusPart Continuous.measurable Prod.opensMeasurableSpace Pi.opensMeasurableSpace Subtype.countable Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace secondCountable_of_proper Complex.instProperSpace Complex.borelSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable Prod.borelSpace Pi.borelSpace ContinuousLinearEquiv.continuous negAt_preimage
measurableSet_plusPart 📖	mathematical	MeasurableSet mixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace	plusPart	—	Set.ext MeasurableSet.inter MeasurableSet.iInter Subtype.countable Finite.to_countable Finite.of_fintype measurableSet_lt BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid measurable_const Measurable.fun_comp measurable_pi_apply Measurable.fst measurable_id'
mem_idealLattice 📖	mathematical	—	mixedSpace Submodule Int.instSemiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup SetLike.instMembership Submodule.setLike idealLattice Set Set.instMembership SetLike.coe FractionalIdeal NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield FractionalIdeal.instSetLike Units.val MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring Prod.instNonAssocSemiring Pi.nonAssocSemiring Real.semiring Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain RingHomSurjective.ids
mem_negAt_plusPart_of_mem 📖	mathematical	mixedSpace Set Set.instMembership Norm.norm Real Real.norm	Set.image DFunLike.coe ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt plusPart Real.instLT Real.instZero	—	RingHomInvPair.ids neg_of_mem_negA_plusPart pos_of_notMem_negAt_plusPart norm_pos_iff negAt_apply_isReal_and_mem abs_of_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_neg negAt_apply_isReal_and_notMem abs_of_pos
mem_rat_span_latticeBasis 📖	mathematical	—	mixedSpace Submodule Rat.semiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Rat.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing NormedAlgebra.toNormedSpace normedAlgebraRat NormedField.toNormedDivisionRing Real.normedField RCLike.charZero_rclike Real.instRCLike RCLike.toNormedAlgebra Complex.instCharZero Complex.instRCLike SetLike.instMembership Submodule.setLike Submodule.span Set.range Module.Free.ChooseBasisIndex NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt DFunLike.coe Module.Basis Real.semiring InnerProductSpace.toNormedSpace RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Module.Basis.instFunLike latticeBasis RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding	—	RCLike.charZero_rclike Complex.instCharZero NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt NumberField.to_charZero RingHomInvPair.ids Module.Basis.sum_repr map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr map_rat_smul Submodule.sum_smul_mem Submodule.subset_span latticeBasis_apply Set.mem_range_self
mem_span_fractionalIdealLatticeBasis 📖	mathematical	—	mixedSpace Submodule Int.instSemiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup SetLike.instMembership Submodule.setLike Submodule.span Set.range Module.Free.ChooseBasisIndex NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield FractionalIdeal.coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero Units.val FractionalIdeal MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Submodule.addCommMonoid Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule DFunLike.coe Module.Basis Real.semiring Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Module.Basis.instFunLike fractionalIdealLatticeBasis Set Set.instMembership Set.image RingHom Semiring.toNonAssocSemiring Prod.instNonAssocSemiring Pi.nonAssocSemiring Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding SetLike.coe FractionalIdeal.instSetLike	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule NumberField.to_charZero Set.range_comp fractionalIdealLatticeBasis_apply RingHomSurjective.ids Submodule.map_span SetLike.mem_coe Submodule.map_coe Set.ext
mem_span_latticeBasis 📖	mathematical	—	mixedSpace Submodule Int.instSemiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup SetLike.instMembership Submodule.setLike Submodule.span Set.range Module.Free.ChooseBasisIndex NumberField.RingOfIntegers NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt DFunLike.coe Module.Basis Real.semiring Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Module.Basis.instFunLike latticeBasis integerLattice	—	NumberField.RingOfIntegers.instFreeInt NumberField.to_charZero Set.range_comp latticeBasis_apply RingHomSurjective.ids Submodule.map_span SetLike.mem_coe Submodule.map_coe NumberField.mem_span_integralBasis
mixedEmbedding_apply_isComplex 📖	mathematical	—	DFunLike.coe RingHom mixedSpace Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.InfinitePlace.embedding	—	—
mixedEmbedding_apply_isReal 📖	mathematical	—	DFunLike.coe RingHom mixedSpace Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.InfinitePlace.embedding_of_isReal Subtype.prop	—	Subtype.prop
mixedSpaceOfRealSpace_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid 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 mixedSpaceOfRealSpace Complex.ofReal	—	—
negAt_apply_isComplex 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids mixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt	—	RingHomInvPair.ids
negAt_apply_isReal_and_mem 📖	mathematical	NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Set Set.instMembership	DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids mixedSpace instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt Real.instNeg	—	RingHomInvPair.ids ContinuousLinearEquiv.neg_apply
negAt_apply_isReal_and_notMem 📖	mathematical	NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Set Set.instMembership	DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids mixedSpace instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt	—	RingHomInvPair.ids
negAt_apply_norm_isReal 📖	mathematical	—	Norm.norm Real Real.norm DFunLike.coe ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids mixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt	—	RingHomInvPair.ids negAt_apply_isReal_and_mem norm_neg negAt_apply_isReal_and_notMem
negAt_apply_snd 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids mixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt	—	RingHomInvPair.ids
negAt_preimage 📖	mathematical	—	Set.preimage mixedSpace DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt Set.image	—	RingHomInvPair.ids ContinuousLinearEquiv.image_eq_preimage_symm negAt_symm
negAt_signSet_apply_isComplex 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids mixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt signSet	—	RingHomInvPair.ids
negAt_signSet_apply_isReal 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids mixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt signSet Norm.norm Real.norm	—	RingHomInvPair.ids negAt_apply_isReal_and_mem Real.norm_of_nonpos negAt_apply_isReal_and_notMem Real.norm_of_nonneg LT.lt.le lt_of_not_ge
negAt_symm 📖	mathematical	—	ContinuousLinearEquiv.symm Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids mixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex negAt	—	ContinuousLinearEquiv.ext RingHomInvPair.ids negAt_apply_isReal_and_mem ContinuousLinearEquiv.neg_apply negAt_apply_isReal_and_notMem
neg_of_mem_negA_plusPart 📖	mathematical	mixedSpace Set Set.instMembership Set.image DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt plusPart	Real.instLT Real.instZero	—	RingHomInvPair.ids negAt_apply_isReal_and_mem neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
nnnorm_eq_sup_normAtPlace 📖	mathematical	—	NNNorm.nnnorm mixedSpace SeminormedAddGroup.toNNNorm Prod.seminormedAddGroup Pi.seminormedAddGroup NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NumberField.InfinitePlace.IsComplex Complex NormedField.toNormedCommRing Complex.instNormedField Finset.sup NNReal instSemilatticeSupNNReal NNReal.instOrderBot Finset.univ Real.instLE Real.instZero DFunLike.coe MonoidWithZeroHom Prod.instMulZeroOneClass Pi.mulZeroOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace normAtPlace_nonneg	—	Finset.ext normAtPlace_nonneg Finset.sup_union Finset.sup_image Prod.nnnorm_def Pi.nnnorm_def NNReal.eq Subtype.prop normAtPlace_apply_of_isReal Subtype.coe_eta normAtPlace_apply_of_isComplex
normAtAllPlaces_apply 📖	mathematical	—	normAtAllPlaces DFunLike.coe MonoidWithZeroHom 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 normAtPlace	—	—
normAtAllPlaces_eq_of_normAtComplexPlaces_eq 📖	mathematical	normAtComplexPlaces	normAtAllPlaces	—	NumberField.InfinitePlace.isReal_or_isComplex normAtPlace_apply_of_isReal normAtComplexPlaces_apply_isReal normAtPlace_apply_of_isComplex normAtComplexPlaces_apply_isComplex
normAtAllPlaces_image_preimage_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	Set.image mixedSpace realSpace normAtAllPlaces Set.preimage	—	Set.image_preimage_eq_iff normAtAllPlaces_apply normAtPlace_mixedSpaceOfRealSpace
normAtAllPlaces_mixedEmbedding 📖	mathematical	—	normAtAllPlaces DFunLike.coe RingHom mixedSpace Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.InfinitePlace.instFunLikeReal	—	normAtAllPlaces_apply normAtPlace_apply
normAtAllPlaces_mixedSpaceOfRealSpace 📖	mathematical	Real Real.instLE Real.instZero	normAtAllPlaces DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid 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 mixedSpaceOfRealSpace	—	normAtAllPlaces_apply normAtPlace_mixedSpaceOfRealSpace
normAtAllPlaces_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero normAtAllPlaces	—	normAtPlace_nonneg
normAtAllPlaces_normAtAllPlaces 📖	mathematical	—	normAtAllPlaces DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid 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 mixedSpaceOfRealSpace	—	normAtAllPlaces_mixedSpaceOfRealSpace normAtAllPlaces_nonneg
normAtAllPlaces_norm_at_real_places 📖	mathematical	—	normAtAllPlaces Norm.norm Real Real.norm	—	NumberField.InfinitePlace.isReal_or_isComplex normAtPlace_apply_of_isReal norm_norm normAtPlace_apply_of_isComplex
normAtComplexPlaces_apply_isComplex 📖	mathematical	—	normAtComplexPlaces NumberField.InfinitePlace NumberField.InfinitePlace.IsComplex Norm.norm Complex Complex.instNorm	—	normAtComplexPlaces.eq_1 NumberField.InfinitePlace.not_isReal_iff_isComplex Subtype.prop normAtPlace_apply_of_isComplex
normAtComplexPlaces_apply_isReal 📖	mathematical	—	normAtComplexPlaces NumberField.InfinitePlace NumberField.InfinitePlace.IsReal	—	normAtComplexPlaces.eq_1
normAtComplexPlaces_mixedSpaceOfRealSpace 📖	mathematical	Real Real.instLE Real.instZero	normAtComplexPlaces DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid 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 mixedSpaceOfRealSpace	—	NumberField.InfinitePlace.isReal_or_isComplex normAtComplexPlaces_apply_isReal mixedSpaceOfRealSpace_apply normAtComplexPlaces_apply_isComplex Complex.norm_of_nonneg
normAtComplexPlaces_normAtAllPlaces 📖	mathematical	—	normAtComplexPlaces DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring realSpace Pi.topologicalSpace NumberField.InfinitePlace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid 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 mixedSpaceOfRealSpace normAtAllPlaces	—	normAtComplexPlaces_mixedSpaceOfRealSpace normAtAllPlaces_nonneg
normAtPlace_add_le 📖	mathematical	—	Real Real.instLE DFunLike.coe MonoidWithZeroHom mixedSpace Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace Prod.instAdd Pi.instAdd Real.instAdd Complex.instAdd	—	normAtPlace.eq_1 norm_add_le
normAtPlace_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 normAtPlace RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.InfinitePlace.instFunLikeReal	—	NumberField.InfinitePlace.norm_embedding_of_isReal NumberField.InfinitePlace.norm_embedding_eq
normAtPlace_apply_of_isComplex 📖	mathematical	NumberField.InfinitePlace.IsComplex	DFunLike.coe MonoidWithZeroHom mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring Complex Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace Norm.norm Complex.instNorm	—	normAtPlace.eq_1 NumberField.InfinitePlace.not_isReal_iff_isComplex
normAtPlace_apply_of_isReal 📖	mathematical	NumberField.InfinitePlace.IsReal	DFunLike.coe MonoidWithZeroHom mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace Norm.norm Real.norm	—	normAtPlace.eq_1
normAtPlace_mixedSpaceOfRealSpace 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe MonoidWithZeroHom mixedSpace Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace ContinuousLinearMap RingHom.id 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 mixedSpaceOfRealSpace	—	NumberField.InfinitePlace.isReal_or_isComplex normAtPlace_apply_of_isReal Real.norm_of_nonneg normAtPlace_apply_of_isComplex Complex.norm_of_nonneg
normAtPlace_neg 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 normAtPlace Prod.instNeg Pi.instNeg Real.instNeg Complex.instNeg	—	normAtPlace.eq_1 norm_neg
normAtPlace_negAt 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 normAtPlace ContinuousLinearEquiv RingHom.id RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt	—	RingHomInvPair.ids NumberField.InfinitePlace.isReal_or_isComplex normAtPlace_apply_of_isReal negAt_apply_norm_isReal normAtPlace_apply_of_isComplex
normAtPlace_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero DFunLike.coe MonoidWithZeroHom mixedSpace Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace	—	normAtPlace.eq_1 norm_nonneg
normAtPlace_real 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 normAtPlace Complex.ofReal abs Real.lattice Real.instAddGroup	—	mul_one normAtPlace_smul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass
normAtPlace_smul 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 normAtPlace Prod.instSMul Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike Real.instMul abs Real.lattice Real.instAddGroup	—	normAtPlace.eq_1 norm_mul NormedDivisionRing.toNormMulClass Complex.norm_mul Complex.norm_real
norm_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 norm Finset.prod Real.instCommMonoid Finset.univ NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Monoid.toNatPow Real.instMonoid normAtPlace NumberField.InfinitePlace.mult	—	—
norm_eq_norm 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 norm RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring RingHom.instFunLike NumberField.mixedEmbedding Real.instRatCast abs Rat.instLattice Rat.addGroup MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring Rat.commRing MonoidHom.instFunLike Algebra.norm DivisionRing.toRatAlgebra NumberField.to_charZero	—	NumberField.to_charZero Finset.prod_congr normAtPlace_apply NumberField.InfinitePlace.prod_eq_abs_norm
norm_eq_of_normAtPlace_eq 📖	mathematical	DFunLike.coe MonoidWithZeroHom 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 normAtPlace	norm	—	Finset.prod_congr
norm_eq_sup'_normAtPlace 📖	mathematical	—	Norm.norm mixedSpace Prod.toNorm NormedRing.toNorm Pi.normedRing NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype NormedCommRing.toNormedRing Real.normedCommRing NumberField.InfinitePlace.IsComplex Complex NormedField.toNormedCommRing Complex.instNormedField Finset.sup' Real.instSemilatticeSup Finset.univ Finset.univ_nonempty NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHom Complex.instField Complex.instCharZero Complex.isAlgClosed DFunLike.coe MonoidWithZeroHom Prod.instMulZeroOneClass Pi.mulZeroOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace	—	Finset.univ_nonempty NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed coe_nnnorm normAtPlace_nonneg nnnorm_eq_sup_normAtPlace Finset.sup'_eq_sup NNReal.val_eq_coe OrderHom.Subtype.val_coe map_finset_sup' LatticeHomClass.toSupHomClass OrderHomClass.toLatticeHomClass OrderHom.instOrderHomClass Finset.sup'_congr
norm_eq_zero_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 norm Real.instZero normAtPlace	—	Real.instNontrivial NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass pow_eq_zero_iff NumberField.InfinitePlace.mult_ne_zero isReduced_of_noZeroDivisors
norm_eq_zero_iff' 📖	mathematical	mixedSpace Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding	MonoidWithZeroHom Prod.instMulZeroOneClass Pi.mulZeroOneClass NonAssocSemiring.toMulZeroOneClass MonoidWithZeroHom.funLike norm Real.instZero Prod.instZero Pi.instZero Complex.instZero	—	NumberField.to_charZero norm_eq_norm Rat.cast_abs Real.instIsStrictOrderedRing abs_eq_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Rat.cast_eq_zero RCLike.charZero_rclike Algebra.norm_eq_zero_iff Rat.isDomain instIsDomain Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule NumberField.to_finiteDimensional instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors map_eq_zero instNontrivialMixedSpace RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
norm_ne_zero_iff 📖	—	—	—	—	not_iff_not
norm_negAt 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 norm ContinuousLinearEquiv RingHom.id RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt	—	norm_eq_of_normAtPlace_eq RingHomInvPair.ids normAtPlace_negAt
norm_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero DFunLike.coe MonoidWithZeroHom mixedSpace Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike norm	—	Finset.prod_nonneg Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_nonneg normAtPlace_nonneg
norm_real 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 norm Complex.ofReal Monoid.toNatPow Real.instMonoid abs Real.lattice Real.instAddGroup Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	NumberField.to_charZero mul_one norm_smul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass
norm_smul 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 norm Prod.instSMul Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike Real.instMul Monoid.toNatPow Real.instMonoid abs Real.lattice Real.instAddGroup Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	NumberField.to_charZero Finset.prod_congr normAtPlace_smul mul_pow Finset.prod_mul_distrib Finset.prod_pow_eq_pow_sum NumberField.InfinitePlace.sum_mult_eq
norm_unit 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom 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 norm RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring 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 Real.instOne	—	NumberField.to_charZero norm_eq_norm NumberField.Units.norm Rat.cast_one
pos_of_notMem_negAt_plusPart 📖	mathematical	mixedSpace Set Set.instMembership Set.image DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt plusPart	Real.instLT Real.instZero	—	RingHomInvPair.ids negAt_apply_isReal_and_notMem
span_idealLatticeBasis 📖	mathematical	—	Submodule.span mixedSpace Int.instSemiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup Set.range Module.Free.ChooseBasisIndex Submodule NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield SetLike.instMembership Submodule.setLike FractionalIdeal.coeToSubmodule nonZeroDivisors Semiring.toMonoidWithZero Units.val FractionalIdeal MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Submodule.addCommMonoid Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule DFunLike.coe Module.Basis Real.semiring Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Module.Basis.instFunLike fractionalIdealLatticeBasis idealLattice	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Submodule.ext NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule RingHomSurjective.ids
span_latticeBasis 📖	mathematical	—	Submodule.span mixedSpace Int.instSemiring Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup Set.range Module.Free.ChooseBasisIndex NumberField.RingOfIntegers NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt DFunLike.coe Module.Basis Real.semiring Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Module.Basis.instFunLike latticeBasis integerLattice	—	NumberField.RingOfIntegers.instFreeInt Submodule.ext_iff mem_span_latticeBasis
stdBasis_apply_isComplex_fst 📖	mathematical	—	DFunLike.coe Finsupp index Real MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Real.semiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids mixedSpace Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr stdBasis Complex.re	—	RingHomInvPair.ids
stdBasis_apply_isComplex_snd 📖	mathematical	—	DFunLike.coe Finsupp index Real MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Real.semiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids mixedSpace Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr stdBasis Complex.im	—	RingHomInvPair.ids
stdBasis_apply_isReal 📖	mathematical	—	DFunLike.coe Finsupp index Real MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Real.semiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids mixedSpace Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr stdBasis	—	RingHomInvPair.ids
stdBasis_repr_eq_matrixToStdBasis_mul 📖	mathematical	DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing NumberField.ComplexEmbedding.conjugate	Complex.ofReal Finsupp index Real MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Real.semiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids mixedSpace Prod.instAddCommMonoid Pi.addCommMonoid NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid NumberField.InfinitePlace.IsComplex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr stdBasis LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring LinearMap.instFunLike commMap Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instFintypeSum Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype instFintypeProd Fin.fintype matrixToStdBasis Equiv Equiv.instEquivLike indexEquiv	—	RingHomInvPair.ids Finset.sum_congr Fintype.sum_sum_type Finset.sum_product Fin.sum_univ_two Matrix.smul_cons mul_one Matrix.smul_empty ite_mul one_mul MulZeroClass.zero_mul Finset.sum_ite_eq add_zero Finset.sum_const_zero NumberField.InfinitePlace.conjugate_embedding_eq_of_isReal Subtype.prop Fintype.complete Nat.instAtLeastTwoHAddOfNat Complex.re_eq_add_conj mul_neg Matrix.cons_val' Matrix.empty_val' Matrix.cons_val_fin_one Finset.sum_add_distrib zero_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Complex.im_eq_sub_conj neg_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.Ring.neg_congr Complex.inv_I one_div Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one neg_div neg_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
volume_eq_two_pow_mul_volume_plusPart 📖	mathematical	mixedSpace Set Set.instMembership Norm.norm Real Real.norm MeasurableSet Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.borelSpace ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume 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 plusPart	—	Complex.instFiniteDimensionalReal Complex.borelSpace Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids MeasureTheory.measure_congr MeasureTheory.Measure.instOuterMeasureClass iUnion_negAt_plusPart_ae MeasureTheory.measure_iUnion Finite.to_countable Set.instFinite Subtype.finite Finite.of_fintype disjoint_negAt_plusPart measurableSet_negAt_plusPart volume_negAt_plusPart tsum_fintype SummationFilter.instLeAtTopUnconditional Finset.sum_const Fintype.card_set nsmul_eq_mul Nat.cast_pow
volume_eq_zero 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure 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 setOf Real.instZero instZeroENNReal	—	add_zero MulZeroClass.mul_zero Complex.instFiniteDimensionalReal Complex.borelSpace MeasureTheory.Measure.addHaar_affineSubspace Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite FiniteDimensional.rclike_to_real instIsAddHaarMeasureMixedSpaceVolume NeZero.charZero_one RCLike.charZero_rclike Set.mem_univ
volume_fundamentalDomain_stdBasis 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure 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 ZSpan.fundamentalDomain index Real.normedField Prod.normedAddCommGroup Pi.normedAddCommGroup Real.normedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal NormedField.toNormedCommRing Complex.instNormedField stdBasis Real.linearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Complex.instFiniteDimensionalReal Complex.borelSpace fundamentalDomain_stdBasis MeasureTheory.Measure.volume_eq_prod MeasureTheory.Measure.prod_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.instSigmaFiniteForallVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper MeasureTheory.volume_pi MeasureTheory.Measure.pi_pi FiniteDimensional.rclike_to_real Real.borelSpace instIsTopologicalAddGroupReal instSecondCountableTopologyReal instProperSpaceReal MeasureTheory.MeasurePreserving.measure_preimage Complex.volume_preserving_equiv_pi MeasurableSet.nullMeasurableSet MeasurableSet.pi Set.countable_univ instCountableFin measurableSet_Ico BorelSpace.opensMeasurable instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Real.volume_Ico sub_zero ENNReal.ofReal_one Finset.prod_const_one one_mul
volume_negAt_plusPart 📖	mathematical	MeasurableSet mixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.borelSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.image ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt plusPart	—	Complex.instFiniteDimensionalReal Complex.borelSpace RingHomInvPair.ids negAt_symm ContinuousLinearEquiv.image_symm_eq_preimage MeasureTheory.MeasurePreserving.measure_preimage volume_preserving_negAt MeasurableSet.nullMeasurableSet measurableSet_plusPart
volume_preserving_negAt 📖	mathematical	—	MeasureTheory.MeasurePreserving mixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace DFunLike.coe ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike negAt MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace measureSpaceOfInnerProductSpace Complex.instFiniteDimensionalReal Complex.borelSpace	—	MeasureTheory.MeasurePreserving.prod Complex.instFiniteDimensionalReal Complex.borelSpace MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.instSigmaFiniteForallVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal SeminormedAddCommGroup.toIsTopologicalAddGroup secondCountable_of_proper Complex.instProperSpace RingHomInvPair.ids MeasureTheory.volume_preserving_pi MeasureTheory.Measure.measurePreserving_neg ContinuousNeg.measurableNeg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.MeasurePreserving.id

NumberField.mixedEmbedding.euclidean

Definitions

Name	Category	Theorems
instRingMixedSpace 📖	CompOp	1 math math: finrank
integerLattice 📖	CompOp	2 math math: instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, instIsZLatticeRealMixedSpaceIntegerLattice
mixedSpace 📖	CompOp	7 math math: stdOrthonormalBasis_map_eq, volumePreserving_toMixed, instNontrivialMixedSpace, instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, instIsZLatticeRealMixedSpaceIntegerLattice, finrank, volumePreserving_toMixed_symm
stdOrthonormalBasis 📖	CompOp	1 math math: stdOrthonormalBasis_map_eq
toMixed 📖	CompOp	3 math math: stdOrthonormalBasis_map_eq, volumePreserving_toMixed, volumePreserving_toMixed_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank 📖	mathematical	—	Module.finrank Real mixedSpace Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingMixedSpace WithLp.instModule ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal EuclideanSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Complex NumberField.InfinitePlace.IsComplex Prod.instAddCommGroup WithLp.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup Prod.instModule AddCommGroup.toAddCommMonoid Pi.Function.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Real.instRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Rat.semiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	NumberField.to_charZero fact_one_le_two_ennreal LinearEquiv.finrank_eq RingHomInvPair.ids NumberField.mixedEmbedding.finrank
instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice 📖	mathematical	—	DiscreteTopology mixedSpace Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid WithLp.instProdTopologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal EuclideanSpace Real NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Complex NumberField.InfinitePlace.IsComplex PiLp.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithLp.instProdNormedAddCommGroup fact_one_le_two_ennreal PiLp.normedAddCommGroup Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup Complex.instNormedAddCommGroup AddCommGroup.toIntModule WithLp.instAddCommGroup Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Complex.addCommGroup SetLike.instMembership Submodule.setLike integerLattice instTopologicalSpaceSubtype	—	fact_one_le_two_ennreal RingHomInvPair.ids integerLattice.eq_1 instDiscreteTopologySubtypeMemSubmoduleIntComap NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice
instIsZLatticeRealMixedSpaceIntegerLattice 📖	mathematical	—	IsZLattice Real Real.normedField mixedSpace WithLp.instProdNormedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal EuclideanSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Complex NumberField.InfinitePlace.IsComplex fact_one_le_two_ennreal PiLp.normedAddCommGroup Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup Complex.instNormedAddCommGroup WithLp.instProdNormedSpace PiLp.seminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedCommRing Complex.instNormedField PiLp.normedSpace InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex integerLattice instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice	—	fact_one_le_two_ennreal instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice RingHomInvPair.ids instIsZLatticeComap NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice
instNontrivialMixedSpace 📖	mathematical	—	Nontrivial mixedSpace	—	Equiv.nontrivial fact_one_le_two_ennreal RingHomInvPair.ids NumberField.mixedEmbedding.instNontrivialMixedSpace
stdOrthonormalBasis_map_eq 📖	mathematical	—	Module.Basis.map NumberField.mixedEmbedding.index Real mixedSpace NumberField.mixedEmbedding.mixedSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup WithLp.instProdNormedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal EuclideanSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Complex NumberField.InfinitePlace.IsComplex fact_one_le_two_ennreal PiLp.normedAddCommGroup Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup Complex.instNormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace WithLp.instProdInnerProductSpace PiLp.innerProductSpace RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instModule Real.semiring Pi.Function.module Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing OrthonormalBasis.toBasis instFintypeSum instFintypeProd Fin.fintype stdOrthonormalBasis ContinuousLinearEquiv.toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithLp.instProdTopologicalSpace PiLp.topologicalSpace Real.pseudoMetricSpace instTopologicalSpaceProd Pi.topologicalSpace WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.addCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Real.instRing toMixed NumberField.mixedEmbedding.stdBasis	—	Module.Basis.eq_of_apply_eq fact_one_le_two_ennreal RingHomInvPair.ids
volumePreserving_toMixed 📖	mathematical	—	MeasureTheory.MeasurePreserving mixedSpace NumberField.mixedEmbedding.mixedSpace WithLp.measurableSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal EuclideanSpace Real NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Complex NumberField.InfinitePlace.IsComplex Prod.instMeasurableSpace MeasurableSpace.pi Real.measurableSpace Complex.measurableSpace DFunLike.coe ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithLp.instProdTopologicalSpace PiLp.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid WithLp.instProdNormedAddCommGroup fact_one_le_two_ennreal PiLp.normedAddCommGroup Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup Complex.instNormedAddCommGroup instTopologicalSpaceProd Pi.topologicalSpace Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup Prod.instModule Pi.addCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Real.instRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex EquivLike.toFunLike ContinuousLinearEquiv.equivLike toMixed MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace WithLp.instProdInnerProductSpace PiLp.innerProductSpace WithLp.instModuleFinite DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Real.instDivisionRing Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid Module.Finite.prod Pi.module FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real Complex.instFiniteDimensionalReal WithLp.borelSpace PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace PiLp.borelSpace Subtype.countable Finite.to_countable Real.borelSpace instSecondCountableTopologyReal Complex.borelSpace UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace secondCountableTopologyEither_of_right PiLp.secondCountableTopology MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Real.measureSpace	—	RingHomInvPair.ids fact_one_le_two_ennreal WithLp.instModuleFinite Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real Complex.instFiniteDimensionalReal WithLp.borelSpace PiLp.borelSpace Subtype.countable Finite.to_countable Real.borelSpace instSecondCountableTopologyReal Complex.borelSpace UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace secondCountableTopologyEither_of_right PiLp.secondCountableTopology Continuous.measurable BorelSpace.opensMeasurable Prod.borelSpace Pi.borelSpace TopologicalSpace.instSecondCountableTopologyForallOfCountable ContinuousLinearEquiv.continuous OrthonormalBasis.addHaar_eq_volume Module.Basis.map_addHaar TopologicalSpace.instSecondCountableTopologyProd instSigmaCompactSpaceProd instSigmaCompactSpaceForallOfFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal sigmaCompactSpace_of_locallyCompact_secondCountable stdOrthonormalBasis_map_eq Module.Basis.addHaar_eq_iff MeasureTheory.Measure.instSigmaFiniteProdVolume MeasureTheory.Measure.instSigmaFiniteForallVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume Module.Basis.coe_parallelepiped MeasureTheory.measure_congr MeasureTheory.Measure.instOuterMeasureClass ZSpan.fundamentalDomain_ae_parallelepiped NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis
volumePreserving_toMixed_symm 📖	mathematical	—	MeasureTheory.MeasurePreserving NumberField.mixedEmbedding.mixedSpace mixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace WithLp.measurableSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal EuclideanSpace DFunLike.coe ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup WithLp.instProdTopologicalSpace PiLp.topologicalSpace WithLp.instProdNormedAddCommGroup fact_one_le_two_ennreal PiLp.normedAddCommGroup Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup Prod.instModule Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup Pi.addCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Real.instRing EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm toMixed MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Real.measureSpace measureSpaceOfInnerProductSpace Complex.instFiniteDimensionalReal Complex.borelSpace WithLp.instProdInnerProductSpace PiLp.innerProductSpace WithLp.instModuleFinite DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Real.instDivisionRing Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid Module.Finite.prod Pi.module FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real WithLp.borelSpace PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace PiLp.borelSpace Subtype.countable Finite.to_countable Real.borelSpace instSecondCountableTopologyReal UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace secondCountableTopologyEither_of_right PiLp.secondCountableTopology	—	WithLp.borelSpace PiLp.borelSpace Subtype.countable Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal Complex.borelSpace secondCountable_of_proper Complex.instProperSpace secondCountableTopologyEither_of_right PiLp.secondCountableTopology Prod.borelSpace Pi.borelSpace TopologicalSpace.instSecondCountableTopologyForallOfCountable RingHomInvPair.ids fact_one_le_two_ennreal WithLp.instModuleFinite Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite FiniteDimensional.rclike_to_real Complex.instFiniteDimensionalReal UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace volumePreserving_toMixed MeasureTheory.MeasurePreserving.symm

NumberField.mixedEmbedding.realSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
volume_eq_zero 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure NumberField.mixedEmbedding.realSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume setOf Real.instZero instZeroENNReal	—	add_zero MulZeroClass.mul_zero MeasureTheory.Measure.addHaar_affineSubspace Pi.borelSpace Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace FiniteDimensional.finiteDimensional_pi' FiniteDimensional.rclike_to_real 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 NeZero.charZero_one RCLike.charZero_rclike Set.mem_univ

---

← Back to Index