Documentation Verification Report

Asymptotics

📁 Source: Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean

Statistics

Metric	Count
Definitions	0
Theorems `tendsto_norm_le_and_mk_eq_div_atTop`, `tendsto_norm_le_div_atTop`, `tendsto_norm_le_div_atTop₀`	3
Total	3

NumberField.Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_norm_le_and_mk_eq_div_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `Nat.card` `Ideal` `NumberField.RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `Real.instLE` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `ClassGroup` `NumberField.RingOfIntegers.instIsDomain` `MonoidHom` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupClassGroup` `MonoidHom.instFunLike` `Filter.atTop` `Real.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `NumberField.InfinitePlace.nrRealPlaces` `Real.pi` `NumberField.InfinitePlace.nrComplexPlaces` `NumberField.Units.regulator` `NumberField.Units.torsionOrder` `Real.sqrt` `abs` `Real.lattice` `Real.instAddGroup` `Real.instIntCast` `NumberField.discr`	—	`NumberField.RingOfIntegers.instIsDomain` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `Set.ext` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instFreeInt` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_ne_zero` `RCLike.charZero_rclike` `Ideal.absNorm_ne_zero_of_nonZeroDivisors` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `NumberField.RingOfIntegers.instIsFractionRing` `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` `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` `PiLp.secondCountableTopology` `IsScalarTower.right` `Nat.card_congr` `Nat.cast_mul` `div_eq_mul_inv` `mul_inv` `mul_comm` `mul_assoc` `inv_mul_cancel_left₀` `NumberField.Units.torsionOrder_ne_zero` `inv_mul_cancel₀` `mul_one` `MeasureTheory.measureReal_def` `UniformSpace.secondCountable_of_separable` `MeasureTheory.MeasurePreserving.measure_preimage` `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed` `MeasurableSet.nullMeasurableSet` `NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne` `NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne` `ZLattice.covolume_comap` `Prod.borelSpace` `Pi.borelSpace` `TopologicalSpace.instSecondCountableTopologyForallOfCountable` `NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice` `NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice` `NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume` `instIsAddHaarMeasureVolume` `NumberField.mixedEmbedding.covolume_idealLattice` `ENNReal.toReal_mul` `ENNReal.toReal_pow` `ENNReal.toReal_ofNat` `ENNReal.coe_toReal` `NNReal.coe_real_pi` `ENNReal.toReal_ofReal` `LT.lt.le` `NumberField.Units.regulator_pos` `FractionalIdeal.coe_mk0` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `FractionalIdeal.coeIdeal_absNorm` `Rat.cast_natCast` `inv_pow` `inv_inv` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `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_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `add_zero` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Mathlib.Tactic.Ring.one_pow` `mul_inv_cancel_right₀` `Filter.Tendsto.comp` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ZLattice.covolume.tendsto_card_le_div'` `instDiscreteTopologySubtypeMemSubmoduleIntComap` `instIsZLatticeComap` `NumberField.mixedEmbedding.euclidean.instNontrivialMixedSpace` `Set.mem_preimage` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem` `LT.lt.ne'` `NumberField.to_charZero` `NumberField.mixedEmbedding.norm_smul` `NumberField.mixedEmbedding.euclidean.finrank` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `AntilipschitzWith.isBounded_preimage` `RingHomIsometric.ids` `ContinuousLinearEquiv.antilipschitz` `NumberField.mixedEmbedding.fundamentalCone.isBounded_normLeOne` `Continuous.measurable` `BorelSpace.opensMeasurable` `ContinuousLinearEquiv.continuous` `ContinuousLinearEquiv.coe_toHomeomorph` `Homeomorph.preimage_frontier` `measurableSet_frontier` `Prod.opensMeasurableSpace` `Pi.opensMeasurableSpace` `NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne` `tendsto_const_nhds` `Filter.Tendsto.atTop_mul_const'` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `Nat.cast_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `Ideal.absNorm_pos_of_nonZeroDivisors` `Filter.tendsto_id`
`tendsto_norm_le_div_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `Nat.card` `Ideal` `NumberField.RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Real.instLE` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Filter.atTop` `Real.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `NumberField.InfinitePlace.nrRealPlaces` `Real.pi` `NumberField.InfinitePlace.nrComplexPlaces` `NumberField.Units.regulator` `NumberField.classNumber` `NumberField.Units.torsionOrder` `Real.sqrt` `abs` `Real.lattice` `Real.instAddGroup` `Real.instIntCast` `NumberField.discr`	—	`NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Nat.instAtLeastTwoHAddOfNat` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_norm_le_div_atTop₀` `tendsto_inv_atTop_zero` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `Filter.Tendsto.congr'` `add_zero` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `Nat.le_floor_iff` `Ideal.card_norm_le_eq_card_norm_le_add_one` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `NumberField.RingOfIntegers.instCharZero_1` `NumberField.to_charZero` `Nat.cast_add` `Nat.cast_one` `add_div` `one_div`
`tendsto_norm_le_div_atTop₀` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `Nat.card` `Ideal` `NumberField.RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `Real.instLE` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Filter.atTop` `Real.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `NumberField.InfinitePlace.nrRealPlaces` `Real.pi` `NumberField.InfinitePlace.nrComplexPlaces` `NumberField.Units.regulator` `NumberField.classNumber` `NumberField.Units.torsionOrder` `Real.sqrt` `abs` `Real.lattice` `Real.instAddGroup` `Real.instIntCast` `NumberField.discr`	—	`NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Nat.instAtLeastTwoHAddOfNat` `NumberField.RingOfIntegers.instIsDomain` `Finset.sum_const` `Finset.card_univ` `nsmul_eq_mul` `NumberField.classNumber.eq_1` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `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_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Filter.Tendsto.congr'` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `Real.instIsStrictOrderedRing` `Nat.le_floor_iff` `Ideal.finite_setOf_absNorm_le₀` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `NumberField.RingOfIntegers.instCharZero_1` `NumberField.to_charZero` `Finset.sum_congr` `Nat.card_congr` `Nat.card_eq_fintype_card` `Fintype.subtype_card` `Fintype.card.eq_1` `Finset.card_eq_sum_card_fiberwise` `Finset.mem_univ` `Nat.cast_sum` `Finset.sum_div` `tendsto_finset_sum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_norm_le_and_mk_eq_div_atTop`

---

← Back to Index