ConvexBody

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

Statistics

Metric	Count
Definitions ConvexBody, convexBodyLT, convexBodyLT', convexBodyLT'Factor, convexBodyLTFactor, convexBodySum, convexBodySumFactor, convexBodySumFun, minkowskiBound	9
Theorems adjust_f, convexBodyLT'Factor_ne_zero, convexBodyLT'_convex, convexBodyLT'_mem, convexBodyLT'_neg_mem, convexBodyLT'_volume, convexBodyLTFactor_ne_zero, convexBodyLT_convex, convexBodyLT_mem, convexBodyLT_neg_mem, convexBodyLT_volume, convexBodySumFactor_ne_zero, convexBodySumFun_add_le, convexBodySumFun_apply, convexBodySumFun_apply', convexBodySumFun_continuous, convexBodySumFun_eq_zero_iff, convexBodySumFun_neg, convexBodySumFun_nonneg, convexBodySumFun_smul, convexBodySum_compact, convexBodySum_convex, convexBodySum_isBounded, convexBodySum_mem, convexBodySum_neg_mem, convexBodySum_volume, convexBodySum_volume_eq_zero_of_le_zero, exists_ne_zero_mem_ideal_lt, exists_ne_zero_mem_ideal_lt', exists_ne_zero_mem_ideal_of_norm_le, exists_ne_zero_mem_ringOfIntegers_lt, exists_ne_zero_mem_ringOfIntegers_lt', exists_ne_zero_mem_ringOfIntegers_of_norm_le, exists_primitive_element_lt_of_isComplex, exists_primitive_element_lt_of_isReal, minkowskiBound_lt_top, minkowskiBound_pos, norm_le_convexBodySumFun, one_le_convexBodyLT'Factor, one_le_convexBodyLTFactor, volume_fundamentalDomain_fractionalIdealLatticeBasis	41
Total	50

NumberField.mixedEmbedding

Definitions

Name	Category	Theorems
convexBodyLT 📖	CompOp	3 math math: convexBodyLT_volume, convexBodyLT_mem, convexBodyLT_convex
convexBodyLT' 📖	CompOp	3 math math: convexBodyLT'_mem, convexBodyLT'_volume, convexBodyLT'_convex
convexBodyLT'Factor 📖	CompOp	2 math math: convexBodyLT'_volume, one_le_convexBodyLT'Factor
convexBodyLTFactor 📖	CompOp	2 math math: one_le_convexBodyLTFactor, convexBodyLT_volume
convexBodySum 📖	CompOp	6 math math: convexBodySum_volume_eq_zero_of_le_zero, convexBodySum_compact, convexBodySum_isBounded, convexBodySum_convex, convexBodySum_volume, convexBodySum_mem
convexBodySumFactor 📖	CompOp	1 math math: convexBodySum_volume
convexBodySumFun 📖	CompOp	9 math math: convexBodySumFun_add_le, norm_le_convexBodySumFun, convexBodySumFun_apply', convexBodySumFun_apply, convexBodySumFun_smul, convexBodySumFun_neg, convexBodySumFun_continuous, convexBodySumFun_nonneg, convexBodySumFun_eq_zero_iff
minkowskiBound 📖	CompOp	3 math math: NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, minkowskiBound_lt_top, minkowskiBound_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjust_f 📖	mathematical	—	Finset.prod NumberField.InfinitePlace NNReal CommSemiring.toCommMonoid instCommSemiringNNReal Finset.univ NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NumberField.InfinitePlace.mult	—	Function.update_of_ne Finset.mul_prod_erase Finset.mem_univ Function.update_self Finset.prod_congr Finset.ne_of_mem_erase NNReal.rpow_natCast NNReal.rpow_mul inv_mul_cancel₀ NumberField.InfinitePlace.mult.eq_1 Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero NNReal.rpow_one mul_assoc Finset.prod_ne_zero_iff NNReal.instNoZeroDivisors pow_ne_zero isReduced_of_noZeroDivisors mul_one
convexBodyLT'Factor_ne_zero 📖	—	—	—	—	mul_ne_zero NNReal.instNoZeroDivisors pow_ne_zero isReduced_of_noZeroDivisors two_ne_zero CharZero.NeZero.two IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing NNReal.pi_ne_zero
convexBodyLT'_convex 📖	mathematical	—	Convex Real mixedSpace Real.semiring Real.partialOrder 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.instSMul Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike convexBodyLT'	—	Convex.prod convex_pi convex_ball IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Convex.inter convex_halfSpace_re_gt convex_halfSpace_re_lt convex_halfSpace_im_gt convex_halfSpace_im_lt
convexBodyLT'_mem 📖	mathematical	—	mixedSpace Set Set.instMembership convexBodyLT' 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 Real.instLT NumberField.InfinitePlace.instFunLikeReal NNReal.toReal abs Real.lattice Real.instAddGroup Complex.re NumberField.InfinitePlace.embedding Real.instOne Complex.im Monoid.toNatPow Real.instMonoid	—	NumberField.InfinitePlace.embedding_of_isReal_apply NumberField.InfinitePlace.norm_embedding_eq NumberField.InfinitePlace.not_isReal_iff_isComplex Subtype.coe_ne_coe mem_ball_zero_iff Set.mem_setOf_eq Subtype.prop Subtype.coe_eta NumberField.InfinitePlace.ne_of_isReal_isComplex
convexBodyLT'_neg_mem 📖	mathematical	mixedSpace Set Set.instMembership convexBodyLT'	Prod.instNeg Pi.instNeg NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instNeg NumberField.InfinitePlace.IsComplex Complex Complex.instNeg	—	dist_zero_right norm_neg abs_neg
convexBodyLT'_volume 📖	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 convexBodyLT' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal convexBodyLT'Factor Finset.prod NNReal CommSemiring.toCommMonoid instCommSemiringNNReal Finset.univ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NumberField.InfinitePlace.mult	—	Complex.instFiniteDimensionalReal Complex.borelSpace Nat.instAtLeastTwoHAddOfNat FiniteDimensional.rclike_to_real MeasureTheory.MeasurePreserving.measure_preimage MeasureTheory.MeasurePreserving.symm Complex.volume_preserving_equiv_real_prod MeasurableSet.nullMeasurableSet MeasurableSet.inter measurableSet_lt BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Measurable.comp measurable_norm Complex.measurable_re measurable_const Complex.measurable_im Set.ext IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add MeasureTheory.Measure.prod_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Real.volume_Ioo sub_neg_eq_add one_add_one_eq_two ENNReal.ofReal_mul zero_le_two Real.instZeroLEOneClass ENNReal.ofReal_pow NNReal.coe_nonneg ENNReal.ofReal_ofNat ENNReal.ofReal_coe_nnreal Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo MeasureTheory.Measure.instSigmaFiniteForallVolume SeminormedAddCommGroup.toIsTopologicalAddGroup secondCountable_of_proper Complex.instProperSpace MeasureTheory.Measure.pi_pi Finset.prod_congr Real.volume_ball Finset.prod_erase_mul Finset.mem_univ Finset.ne_of_mem_erase Complex.volume_ball Real.instIsOrderedRing Finset.prod_mul_distrib Finset.prod_const Finset.card_erase_of_mem Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 convexBodyLT'Factor.eq_1 pow_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos NumberField.InfinitePlace.prod_eq_prod_mul_prod ENNReal.coe_finset_prod NumberField.InfinitePlace.mult_isReal NumberField.InfinitePlace.mult_isComplex pow_one mul_assoc
convexBodyLTFactor_ne_zero 📖	—	—	—	—	mul_ne_zero NNReal.instNoZeroDivisors pow_ne_zero isReduced_of_noZeroDivisors two_ne_zero CharZero.NeZero.two IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing NNReal.pi_ne_zero
convexBodyLT_convex 📖	mathematical	—	Convex Real mixedSpace Real.semiring Real.partialOrder 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.instSMul Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike convexBodyLT	—	Convex.prod convex_pi convex_ball
convexBodyLT_mem 📖	mathematical	—	mixedSpace Set Set.instMembership convexBodyLT 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 Real.instLT NumberField.InfinitePlace.instFunLikeReal NNReal.toReal	—	NumberField.InfinitePlace.embedding_of_isReal_apply NumberField.InfinitePlace.norm_embedding_eq
convexBodyLT_neg_mem 📖	mathematical	mixedSpace Set Set.instMembership convexBodyLT	Prod.instNeg Pi.instNeg NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instNeg NumberField.InfinitePlace.IsComplex Complex Complex.instNeg	—	norm_neg
convexBodyLT_volume 📖	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 convexBodyLT Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal convexBodyLTFactor Finset.prod NNReal CommSemiring.toCommMonoid instCommSemiringNNReal Finset.univ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NumberField.InfinitePlace.mult	—	Complex.instFiniteDimensionalReal Complex.borelSpace Nat.instAtLeastTwoHAddOfNat 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.Measure.pi_pi FiniteDimensional.rclike_to_real Real.borelSpace instIsTopologicalAddGroupReal instSecondCountableTopologyReal instProperSpaceReal Finset.prod_congr Real.volume_ball Complex.volume_ball ENNReal.ofReal_mul Real.instIsOrderedRing Finset.prod_mul_distrib Finset.prod_const ENNReal.ofReal_ofNat ENNReal.ofReal_coe_nnreal Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul NumberField.InfinitePlace.prod_eq_prod_mul_prod ENNReal.coe_finset_prod NumberField.InfinitePlace.mult_isReal NumberField.InfinitePlace.mult_isComplex pow_one
convexBodySumFactor_ne_zero 📖	—	—	—	—	div_ne_zero NumberField.to_charZero mul_ne_zero NNReal.instNoZeroDivisors pow_ne_zero isReduced_of_noZeroDivisors two_ne_zero CharZero.NeZero.two IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing NNReal.pi_ne_zero Nat.cast_ne_zero Nat.factorial_ne_zero
convexBodySumFun_add_le 📖	mathematical	—	Real Real.instLE convexBodySumFun mixedSpace Prod.instAdd Pi.instAdd NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAdd NumberField.InfinitePlace.IsComplex Complex Complex.instAdd	—	Finset.sum_congr Distrib.leftDistribClass Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing normAtPlace_add_le LT.lt.le Nat.cast_pos Real.instNontrivial NumberField.InfinitePlace.mult_pos
convexBodySumFun_apply 📖	mathematical	—	convexBodySumFun Finset.sum NumberField.InfinitePlace Real Real.instAddCommMonoid Finset.univ NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.instMul Real.instNatCast NumberField.InfinitePlace.mult DFunLike.coe MonoidWithZeroHom mixedSpace Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace	—	—
convexBodySumFun_apply' 📖	mathematical	—	convexBodySumFun Real Real.instAdd Finset.sum NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommMonoid Finset.univ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Norm.norm Real.norm Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat NumberField.InfinitePlace.IsComplex Complex Complex.instNorm	—	Nat.instAtLeastTwoHAddOfNat NumberField.InfinitePlace.sum_eq_sum_add_sum Finset.sum_congr NumberField.InfinitePlace.mult_isReal NumberField.InfinitePlace.mult_isComplex Nat.cast_one one_mul Subtype.prop normAtPlace_apply_of_isReal normAtPlace_apply_of_isComplex Finset.mul_sum
convexBodySumFun_continuous 📖	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 convexBodySumFun	—	continuous_finset_sum IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul continuous_const continuous_id' continuous_normAtPlace
convexBodySumFun_eq_zero_iff 📖	mathematical	—	convexBodySumFun Real Real.instZero mixedSpace Prod.instZero Pi.instZero NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NumberField.InfinitePlace.IsComplex Complex Complex.instZero	—	forall_normAtPlace_eq_zero_iff convexBodySumFun.eq_1 Finset.sum_eq_zero_iff_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le Nat.cast_pos Real.instNontrivial NumberField.InfinitePlace.mult_pos normAtPlace_nonneg mul_left_mem_nonZeroDivisors_eq_zero_iff mem_nonZeroDivisors_iff_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass NumberField.InfinitePlace.mult_coe_ne_zero
convexBodySumFun_neg 📖	mathematical	—	convexBodySumFun mixedSpace Prod.instNeg Pi.instNeg NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instNeg NumberField.InfinitePlace.IsComplex Complex Complex.instNeg	—	Finset.sum_congr normAtPlace_neg
convexBodySumFun_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero convexBodySumFun	—	Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le Nat.cast_pos Real.instNontrivial NumberField.InfinitePlace.mult_pos normAtPlace_nonneg
convexBodySumFun_smul 📖	mathematical	—	convexBodySumFun Real mixedSpace Prod.instSMul Function.hasSMul NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id NumberField.InfinitePlace.IsComplex Complex 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	—	Finset.sum_congr normAtPlace_smul mul_comm Finset.mul_sum mul_assoc
convexBodySum_compact 📖	mathematical	—	IsCompact mixedSpace 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 convexBodySum	—	Metric.isCompact_iff_isClosed_bounded Prod.t2Space Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Complex.instT2Space prod_properSpace pi_properSpace instProperSpaceReal Complex.instProperSpace Set.ext IsClosed.preimage convexBodySumFun_continuous isClosed_Icc HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid convexBodySum_isBounded
convexBodySum_convex 📖	mathematical	—	Convex Real mixedSpace Real.semiring Real.partialOrder 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.instSMul Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike convexBodySum	—	Convex_subadditive_le Real.instIsOrderedRing convexBodySumFun_add_le abs_eq_self Real.instIsOrderedAddMonoid le_of_eq convexBodySumFun_smul
convexBodySum_isBounded 📖	mathematical	—	Bornology.IsBounded mixedSpace Prod.instBornology Pi.instBornology NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField convexBodySum	—	Metric.isBounded_iff le_trans norm_sub_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add norm_le_convexBodySumFun
convexBodySum_mem 📖	mathematical	—	mixedSpace Set Set.instMembership convexBodySum 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 Real.instLE Finset.sum Real.instAddCommMonoid Finset.univ NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.instMul Real.instNatCast NumberField.InfinitePlace.mult AbsoluteValue Real.partialOrder AbsoluteValue.funLike NumberField.place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial	—	Complex.instNontrivial Finset.sum_congr normAtPlace_apply
convexBodySum_neg_mem 📖	mathematical	mixedSpace Set Set.instMembership convexBodySum	Prod.instNeg Pi.instNeg NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instNeg NumberField.InfinitePlace.IsComplex Complex Complex.instNeg	—	Set.mem_setOf convexBodySumFun_neg
convexBodySum_volume 📖	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 convexBodySum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal convexBodySumFactor Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.ofReal 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	—	Complex.instFiniteDimensionalReal Complex.borelSpace NumberField.to_charZero le_or_gt convexBodySum_volume_eq_zero_of_le_zero ENNReal.ofReal_eq_zero zero_pow LT.lt.ne' Module.finrank_pos commRing_strongRankCondition Rat.nontrivial NumberField.to_finiteDimensional Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing MulZeroClass.mul_zero MeasureTheory.measure_le_eq_lt Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real Prod.instIsTopologicalAddGroup Pi.topologicalAddGroup instIsTopologicalAddGroupReal SeminormedAddCommGroup.toIsTopologicalAddGroup Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal Real.borelSpace secondCountable_of_proper Complex.instProperSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable Prod.t2Space Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Complex.instT2Space Prod.continuousSMul instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul instIsAddHaarMeasureMixedSpaceVolume convexBodySumFun_eq_zero_iff convexBodySumFun_neg convexBodySumFun_add_le le_of_eq convexBodySumFun_smul instNontrivialMixedSpace MeasureTheory.measure_lt_one_eq_integral_div_gamma zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike finrank div_one Real.Gamma_nat_eq_factorial ENNReal.ofReal_div_of_pos Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Nat.factorial_pos Real.rpow_one ENNReal.ofReal_natCast Nat.instAtLeastTwoHAddOfNat convexBodySumFun_apply' neg_add Finset.mul_sum Real.exp_add Real.exp_sum MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.instSigmaFiniteForallVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal MeasureTheory.integral_fintype_prod_volume_eq_pow integral_comp_abs integral_exp_neg_rpow Complex.integral_exp_neg_mul_rpow le_rfl zero_lt_two IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid one_add_one_eq_two Real.Gamma_add_one two_ne_zero CharZero.NeZero.two Real.Gamma_two mul_one mul_assoc Real.rpow_add_one Mathlib.Meta.NormNum.isInt_eq_true Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Real.rpow_neg_one div_eq_mul_inv convexBodySumFactor.eq_1 ENNReal.ofReal_mul le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat ENNReal.ofReal_pow zero_le_two div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Real.pi_pos ENNReal.ofReal_ofNat NNReal.coe_real_pi ENNReal.ofReal_coe_nnreal ENNReal.coe_div Nat.cast_ne_zero IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing Nat.factorial_ne_zero ENNReal.coe_mul ENNReal.coe_pow ENNReal.coe_ofNat ENNReal.coe_natCast mul_comm Set.preimage_smul_inv₀ ne_of_gt Finset.sum_congr normAtPlace_smul abs_inv abs_eq_self inv_mul_le_iff₀ abs_pow abs_nonneg covariant_swap_add_of_covariant_add MeasureTheory.Measure.addHaar_smul PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Complex.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace
convexBodySum_volume_eq_zero_of_le_zero 📖	mathematical	Real Real.instLE Real.instZero	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.measureSpace NumberField.InfinitePlace.IsComplex Complex measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume convexBodySum instZeroENNReal	—	Complex.instFiniteDimensionalReal Complex.borelSpace lt_or_eq_of_le Set.ext Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Set.mem_setOf convexBodySumFun_nonneg MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass convexBodySum.eq_1 Set.mem_setOf_eq Set.mem_singleton_iff convexBodySumFun_eq_zero_iff LE.le.ge_iff_eq' MeasureTheory.NoAtoms.measure_singleton instNoAtomsMixedSpaceVolume
exists_ne_zero_mem_ideal_lt 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder minkowskiBound 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 MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume convexBodyLT	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 SetLike.instMembership FractionalIdeal.instSetLike Units.val MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Real.instLT NumberField.InfinitePlace.instFunLikeReal NNReal.toReal	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Complex.instFiniteDimensionalReal Complex.borelSpace NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule ZSpan.isAddFundamentalDomain' Finite.of_fintype NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Prod.opensMeasurableSpace Pi.opensMeasurableSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Complex.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable instCountable_of_discrete_submodule Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite FiniteDimensional.rclike_to_real ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite instIsZLatticeRealSpan MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure Prod.borelSpace Pi.borelSpace instIsAddHaarMeasureMixedSpaceVolume convexBodyLT_neg_mem convexBodyLT_convex mem_span_fractionalIdealLatticeBasis Submodule.mem_toAddSubgroup instNontrivialMixedSpace RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass convexBodyLT_mem
exists_ne_zero_mem_ideal_lt' 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder minkowskiBound 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 MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume convexBodyLT'	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 SetLike.instMembership FractionalIdeal.instSetLike Units.val MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Real.instLT NumberField.InfinitePlace.instFunLikeReal NNReal.toReal abs Real.lattice Real.instAddGroup Complex.re RingHom Semiring.toNonAssocSemiring Complex.instSemiring RingHom.instFunLike NumberField.InfinitePlace.embedding Real.instOne Complex.im Monoid.toNatPow Real.instMonoid	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Complex.instFiniteDimensionalReal Complex.borelSpace NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule ZSpan.isAddFundamentalDomain' Finite.of_fintype NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Prod.opensMeasurableSpace Pi.opensMeasurableSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Complex.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable instCountable_of_discrete_submodule Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite FiniteDimensional.rclike_to_real ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite instIsZLatticeRealSpan MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure Prod.borelSpace Pi.borelSpace instIsAddHaarMeasureMixedSpaceVolume convexBodyLT'_neg_mem convexBodyLT'_convex mem_span_fractionalIdealLatticeBasis Submodule.mem_toAddSubgroup instNontrivialMixedSpace RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass convexBodyLT'_mem
exists_ne_zero_mem_ideal_of_norm_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder minkowskiBound 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 MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume convexBodySum	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 SetLike.instMembership FractionalIdeal.instSetLike Units.val MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Real.instLE Real.instRatCast abs Rat.instLattice Rat.addGroup MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring Rat.commRing MonoidHom.instFunLike Algebra.norm DivisionRing.toRatAlgebra NumberField.to_charZero Monoid.toNatPow Real.instMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Rat.commSemiring	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Complex.instFiniteDimensionalReal Complex.borelSpace Mathlib.Tactic.Contrapose.contrapose₁ convexBodySum_volume_eq_zero_of_le_zero le_of_lt minkowskiBound_pos NumberField.to_charZero inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Module.finrank_pos commRing_strongRankCondition Rat.nontrivial NumberField.to_finiteDimensional Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing div_nonneg Nat.cast_nonneg NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule ZSpan.isAddFundamentalDomain' Finite.of_fintype NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Prod.opensMeasurableSpace Pi.opensMeasurableSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Complex.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable instCountable_of_discrete_submodule Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite FiniteDimensional.rclike_to_real ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite instIsZLatticeRealSpan MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure Prod.borelSpace Pi.borelSpace instNontrivialMixedSpace instIsAddHaarMeasureMixedSpaceVolume ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite convexBodySum_neg_mem convexBodySum_convex convexBodySum_compact mem_span_fractionalIdealLatticeBasis Submodule.mem_toAddSubgroup RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Real.rpow_natCast Real.rpow_le_rpow_iff Rat.cast_abs IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Real.rpow_nonneg Real.rpow_mul mul_inv_cancel₀ Nat.cast_ne_zero RCLike.charZero_rclike ne_of_gt Real.rpow_one le_div_iff₀' le_trans Complex.instNontrivial NumberField.InfinitePlace.sum_mult_eq Nat.cast_sum Finset.prod_congr le_of_eq Real.geom_mean_le_arith_mean AbsoluteValue.nonneg convexBodySum_mem
exists_ne_zero_mem_ringOfIntegers_lt 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder minkowskiBound Units 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 MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Units.instOne 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 MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume convexBodyLT	Real.instLT NumberField.InfinitePlace.instFunLikeReal NumberField.RingOfIntegers.val NNReal.toReal	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Complex.instFiniteDimensionalReal Complex.borelSpace exists_ne_zero_mem_ideal_lt FractionalIdeal.mem_one_iff NumberField.RingOfIntegers.coe_ne_zero_iff
exists_ne_zero_mem_ringOfIntegers_lt' 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder minkowskiBound Units 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 MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Units.instOne 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 MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume convexBodyLT'	Real.instLT NumberField.InfinitePlace.instFunLikeReal NumberField.RingOfIntegers.val NNReal.toReal abs Real.lattice Real.instAddGroup Complex.re RingHom Semiring.toNonAssocSemiring Complex.instSemiring RingHom.instFunLike NumberField.InfinitePlace.embedding Real.instOne Complex.im Monoid.toNatPow Real.instMonoid	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Complex.instFiniteDimensionalReal Complex.borelSpace exists_ne_zero_mem_ideal_lt' FractionalIdeal.mem_one_iff NumberField.RingOfIntegers.coe_ne_zero_iff
exists_ne_zero_mem_ringOfIntegers_of_norm_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder minkowskiBound Units 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 MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Units.instOne 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 MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume convexBodySum	Real.instLE Real.instRatCast abs Rat.instLattice Rat.addGroup MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring Rat.commRing MonoidHom.instFunLike Algebra.norm DivisionRing.toRatAlgebra NumberField.to_charZero NumberField.RingOfIntegers.val Monoid.toNatPow Real.instMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Rat.commSemiring	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Complex.instFiniteDimensionalReal Complex.borelSpace NumberField.to_charZero exists_ne_zero_mem_ideal_of_norm_le FractionalIdeal.mem_one_iff NumberField.RingOfIntegers.coe_ne_zero_iff
exists_primitive_element_lt_of_isComplex 📖	mathematical	NumberField.InfinitePlace.IsComplex ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder minkowskiBound Units 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 MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Units.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.instCommSemiring ENNReal.ofNNReal convexBodyLT'Factor	IntermediateField.adjoin Rat.instField DivisionRing.toRatAlgebra NumberField.to_charZero Set Set.instSingletonSet NumberField.RingOfIntegers.val Top.top IntermediateField OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Real Real.instLT DFunLike.coe NumberField.InfinitePlace NumberField.InfinitePlace.instFunLikeReal Real.sqrt Real.instAdd Real.instOne Monoid.toNatPow Real.instMonoid NNReal.toReal	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Complex.instFiniteDimensionalReal Complex.borelSpace convexBodyLT'_volume Finset.prod_erase_mul Finset.mem_univ Finset.prod_congr ite_pow one_pow Finset.prod_ite_eq' NumberField.InfinitePlace.not_isReal_iff_isComplex one_mul NNReal.sq_sqrt NumberField.to_charZero exists_ne_zero_mem_ringOfIntegers_lt' NumberField.is_primitive_element_of_infinitePlace_lt NumberField.InfinitePlace.norm_embedding_eq Real.lt_sqrt norm_nonneg Complex.re_add_im Complex.norm_add_mul_I Real.sq_sqrt add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add sq_abs sq_lt_one_iff₀ IsStrictOrderedRing.toPosMulStrictMono Real.instZeroLEOneClass abs_nonneg sq_lt_sq NNReal.abs_eq lt_of_lt_of_le NNReal.coe_one Real.le_sqrt' zero_lt_one NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le IsOrderedRing.toPosMulMono Real.instIsOrderedRing
exists_primitive_element_lt_of_isReal 📖	mathematical	NumberField.InfinitePlace.IsReal ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder minkowskiBound Units 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 MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Units.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.instCommSemiring ENNReal.ofNNReal convexBodyLTFactor	IntermediateField.adjoin Rat.instField DivisionRing.toRatAlgebra NumberField.to_charZero Set Set.instSingletonSet NumberField.RingOfIntegers.val Top.top IntermediateField OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Real Real.instLT DFunLike.coe NumberField.InfinitePlace NumberField.InfinitePlace.instFunLikeReal NNReal.toReal NNReal NNReal.instMax instOneNNReal	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Complex.instFiniteDimensionalReal Complex.borelSpace convexBodyLT_volume Finset.prod_erase_mul Finset.mem_univ Finset.prod_congr ite_pow one_pow Finset.prod_ite_eq' one_mul pow_one NumberField.to_charZero exists_ne_zero_mem_ringOfIntegers_lt NumberField.is_primitive_element_of_infinitePlace_lt lt_of_lt_of_le NNReal.coe_max
minkowskiBound_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder minkowskiBound Top.top instTopENNReal	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain ENNReal.mul_lt_top Complex.instFiniteDimensionalReal Complex.borelSpace Bornology.IsBounded.measure_lt_top prod_properSpace pi_properSpace instProperSpaceReal Complex.instProperSpace MeasureTheory.Measure.instIsFiniteMeasureOnCompactsProdVolume MeasureTheory.Measure.instIsFiniteMeasureOnCompactsForallVolumeOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts SeminormedAddCommGroup.toIsTopologicalAddGroup secondCountable_of_proper ZSpan.fundamentalDomain_isBounded Real.instIsStrictOrderedRing Finite.of_fintype NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule instHasSolidNormReal ENNReal.pow_lt_top ENNReal.ofNat_lt_top
minkowskiBound_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal minkowskiBound	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain ENNReal.mul_pos Complex.instFiniteDimensionalReal Complex.borelSpace ZSpan.measure_fundamentalDomain_ne_zero Finite.of_fintype NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal Real.borelSpace PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Complex.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable instIsAddHaarMeasureMixedSpaceVolume ENNReal.pow_ne_zero Nat.instAtLeastTwoHAddOfNat two_ne_zero CharZero.NeZero.two ENNReal.instCharZero
norm_le_convexBodySumFun 📖	mathematical	—	Real Real.instLE Norm.norm mixedSpace Prod.toNorm NormedRing.toNorm Pi.normedRing NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype NormedCommRing.toNormedRing Real.normedCommRing NumberField.InfinitePlace.IsComplex Complex NormedField.toNormedCommRing Complex.instNormedField convexBodySumFun	—	Finset.univ_nonempty NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed norm_eq_sup'_normAtPlace Finset.sup'_le_iff convexBodySumFun_apply Finset.add_sum_erase Finset.mem_univ le_add_of_le_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_mul_of_one_le_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing normAtPlace_nonneg NumberField.InfinitePlace.one_le_mult Finset.sum_nonneg mul_nonneg IsOrderedRing.toPosMulMono LT.lt.le Nat.cast_pos Real.instNontrivial NumberField.InfinitePlace.mult_pos
one_le_convexBodyLT'Factor 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal convexBodyLT'Factor	—	one_le_mul NNReal.mulLeftMono one_le_pow₀ IsStrictOrderedRing.toZeroLEOneClass NNReal.instIsStrictOrderedRing IsOrderedRing.toPosMulMono NNReal.instIsOrderedRing one_le_two NNReal.addLeftMono Real.instZeroLEOneClass Real.instIsOrderedRing LE.le.trans Nat.instAtLeastTwoHAddOfNat IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.two_le_pi
one_le_convexBodyLTFactor 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal convexBodyLTFactor	—	one_le_mul NNReal.mulLeftMono one_le_pow₀ IsStrictOrderedRing.toZeroLEOneClass NNReal.instIsStrictOrderedRing IsOrderedRing.toPosMulMono NNReal.instIsOrderedRing one_le_two NNReal.addLeftMono Real.instZeroLEOneClass Real.instIsOrderedRing LE.le.trans Nat.instAtLeastTwoHAddOfNat IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.two_le_pi
volume_fundamentalDomain_fractionalIdealLatticeBasis 📖	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 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.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 fractionalIdealLatticeBasis Real.linearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.instCommSemiring ENNReal.ofReal Real.instRatCast MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass FractionalIdeal.commSemiring Rat.semiring MonoidWithZeroHom.funLike FractionalIdeal.absNorm NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt latticeBasis	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule NumberField.RingOfIntegers.instFreeInt NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt Module.finrank_eq_card_chooseBasisIndex commRing_strongRankCondition Int.instNontrivial NumberField.fractionalIdeal_rank Complex.instFiniteDimensionalReal Complex.borelSpace ZSpan.fundamentalDomain_reindex ZSpan.measure_fundamentalDomain Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Complex.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable instIsAddHaarMeasureMixedSpaceVolume NumberField.to_charZero Module.Basis.coe_reindex fractionalIdealLatticeBasis_apply det_basisOfFractionalIdeal_eq_norm

(root)

Definitions

Name	Category	Theorems
ConvexBody 📖	CompData	15 math math: ConvexBody.coe_smul, ConvexBody.coe_mk, ConvexBody.convex, ConvexBody.ext_iff, ConvexBody.isBounded, ConvexBody.nonempty, ConvexBody.isClosed, ConvexBody.isCompact, ConvexBody.hausdorffDist_coe, ConvexBody.hausdorffEDist_coe, ConvexBody.hausdorffEdist_coe, ConvexBody.coe_add, ConvexBody.coe_nsmul, ConvexBody.coe_smul', ConvexBody.coe_zero

---

← Back to Index