Documentation Verification Report

ClassNumber

📁 Source: Mathlib/NumberTheory/NumberField/ClassNumber.lean

Statistics

Metric	Count
Definitions `instFintypeClassGroup`, `classNumber`	2
Theorems `classNumber_eq_one_iff`, `classNumber_ne_zero`, `classNumber_pos`, `exists_ideal_in_class_of_norm_le`, `classNumber_eq`, `isPrincipalIdealRing_of_abs_discr_lt`, `isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc`, `isPrincipalIdealRing_of_isPrincipal_of_norm_le`, `isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime`, `isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc`	10
Total	12

NumberField

Definitions

Name	Category	Theorems
`classNumber` 📖	CompOp	6 math math: `dedekindZeta_residue_def`, `classNumber_pos`, `classNumber_eq_one_iff`, `Ideal.tendsto_norm_le_div_atTop₀`, `Ideal.tendsto_norm_le_div_atTop`, `Rat.classNumber_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`classNumber_eq_one_iff` 📖	mathematical	—	`classNumber` `IsPrincipalIdealRing` `RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingOfIntegers.instCommRing`	—	`card_classGroup_eq_one_iff` `RingOfIntegers.instIsDomain` `RingOfIntegers.instIsDedekindDomain`
`classNumber_ne_zero` 📖	—	—	—	—	`Fintype.card_ne_zero` `RingOfIntegers.instIsDomain`
`classNumber_pos` 📖	mathematical	—	`classNumber`	—	`Fintype.card_pos` `RingOfIntegers.instIsDomain`
`exists_ideal_in_class_of_norm_le` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Ideal` `RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingOfIntegers.instCommRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `ClassGroup` `RingOfIntegers.instIsDomain` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupClassGroup` `MonoidHom.instFunLike` `RingOfIntegers.instIsDedekindDomain` `Real` `Real.instLE` `Real.instNatCast` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `RingOfIntegers.instNontrivial` `RingOfIntegers.instFreeInt` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `InfinitePlace.nrComplexPlaces` `Nat.factorial` `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` `to_charZero` `Real.sqrt` `abs` `Real.lattice` `Real.instAddGroup` `Real.instIntCast` `discr`	—	`RingOfIntegers.instIsDomain` `RingOfIntegers.instIsDedekindDomain` `RingOfIntegers.instNontrivial` `RingOfIntegers.instFreeInt` `Nat.instAtLeastTwoHAddOfNat` `to_charZero` `RingOfIntegers.instIsFractionRing` `Module.IsNoetherian.finite` `RingOfIntegers.instIsNoetherianInt` `exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr` `IsScalarTower.right` `Ideal.dvd_iff_le` `Ideal.span_singleton_le_iff_mem` `Mathlib.Tactic.Contrapose.contrapose₄` `Algebra.linearMap_apply` `Ideal.span_singleton_eq_bot` `Ideal.zero_eq_bot` `MulZeroClass.mul_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mem_nonZeroDivisors_iff_ne_zero` `Ideal.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `Ideal.instNontrivial` `Subtype.coe_ne_coe` `mul_comm` `inv_inv` `le_of_mul_le_mul_of_pos_left` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `mul_assoc` `mul_div_assoc` `Rat.cast_natCast` `FractionalIdeal.coeIdeal_absNorm` `FractionalIdeal.coe_mk0` `Ideal.absNorm_apply` `Rat.cast_mul` `RCLike.charZero_rclike` `Nat.cast_mul` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `FractionalIdeal.coeIdeal_span_singleton` `FractionalIdeal.absNorm_span_singleton` `RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `to_finiteDimensional` `Nat.cast_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `pos_of_ne_zero` `Nat.instCanonicallyOrderedAdd` `Ideal.absNorm_ne_zero_of_nonZeroDivisors`

NumberField.RingOfIntegers

Definitions

Name	Category	Theorems
`instFintypeClassGroup` 📖	CompOp	—

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`classNumber_eq` 📖	mathematical	—	`NumberField.classNumber` `instField` `numberField`	—	`numberField` `NumberField.classNumber_eq_one_iff` `IsPrincipalIdealRing.of_surjective` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `EuclideanDomain.to_principal_ideal_domain` `RingEquiv.surjective`

RingOfIntegers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrincipalIdealRing_of_abs_discr_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instIntCast` `abs` `instLatticeInt` `Int.instAddGroup` `NumberField.discr` `Monoid.toNatPow` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi` `NumberField.InfinitePlace.nrComplexPlaces` `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` `Nat.factorial`	`IsPrincipalIdealRing` `NumberField.RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing`	—	`Nat.instAtLeastTwoHAddOfNat` `NumberField.to_charZero` `Module.finrank_pos` `commRing_strongRankCondition` `Rat.nontrivial` `NumberField.to_finiteDimensional` `Rat.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isPrincipalIdealRing_of_isPrincipal_of_norm_le` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Ideal.absNorm_eq_one_iff` `le_antisymm` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `lt_of_le_of_lt` `Int.cast_abs` `Real.instIsStrictOrderedRing` `mul_assoc` `inv_div` `inv_pow` `mul_inv` `inv_mul_lt_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `mul_pos` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `div_pos` `Real.pi_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_pos'` `NeZero.charZero_one` `Nat.factorial_pos` `Real.sqrt_lt` `Int.cast_nonneg` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `abs_nonneg` `Int.instAddLeftMono` `covariant_swap_add_of_covariant_add` `le_of_lt` `Ideal.absNorm_ne_zero_of_nonZeroDivisors` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `top_isPrincipal`
`isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc` 📖	mathematical	`Ideal` `NumberField.RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Set` `Set.instMembership` `Ideal.primesOver` `Int.instCommSemiring` `Ideal.span` `Set.instSingletonSet` `Ring.toIntAlgebra` `CommRing.toRing` `Nat.floor` `Real` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `NumberField.InfinitePlace.nrComplexPlaces` `Nat.factorial` `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` `Real.sqrt` `abs` `Real.lattice` `Real.instAddGroup` `Real.instIntCast` `NumberField.discr` `Nat.instMonoid` `Ideal.inertiaDeg` `Int.instCommRing` `Int.instSemiring` `Submodule.IsPrincipal` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`IsPrincipalIdealRing`	—	`NumberField.to_charZero` `Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc` `Ideal.IsPrime.isMaximal` `IsDedekindDomainDvr.ring_dimensionLEOne` `Int.instIsDomain` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `EuclideanDomain.to_principal_ideal_domain` `Ideal.isPrime_of_prime` `Ideal.prime_span_singleton_iff` `Nat.prime_iff_prime_int` `Nat.Prime.ne_zero` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `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.neg_zero` `Mathlib.Tactic.Ring.sub_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.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_pow` `Ideal.exists_smul_eq_of_isGaloisGroup` `Finite.algEquiv` `Finite.algHom` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Rat.isDomain` `NumberField.to_finiteDimensional` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `instIsDomain` `instIsGaloisGroupIntRingOfIntegersOfRat` `IsGaloisGroup.of_isGalois` `Submodule.IsPrincipal.map_ringHom` `RingHom.instRingHomClass` `Ideal.inertiaDeg_eq_of_isGaloisGroup`
`isPrincipalIdealRing_of_isPrincipal_of_norm_le` 📖	mathematical	`Submodule.IsPrincipal` `NumberField.RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`IsPrincipalIdealRing`	—	`NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Nat.instAtLeastTwoHAddOfNat` `NumberField.to_charZero` `NumberField.classNumber_eq_one_iff` `NumberField.RingOfIntegers.instIsDomain` `NumberField.classNumber.eq_1` `Fintype.card_eq_one_iff` `NumberField.exists_ideal_in_class_of_norm_le` `Subtype.coe_eta`
`isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime` 📖	mathematical	`Submodule.IsPrincipal` `NumberField.RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`IsPrincipalIdealRing`	—	`NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `Nat.instAtLeastTwoHAddOfNat` `NumberField.to_charZero` `isPrincipalIdealRing_of_isPrincipal_of_norm_le` `Ideal.mem_isPrincipalSubmonoid_iff` `Ideal.uniqueFactorizationMonoid` `prod_normalizedFactors_eq_self` `nonZeroDivisors.coe_ne_zero` `Ideal.instNontrivial` `Submonoid.multiset_prod_mem` `bot_isPrincipal` `mem_nonZeroDivisors_of_ne_zero` `Ideal.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `NumberField.RingOfIntegers.instIsDomain` `Ideal.mem_normalizedFactors_iff` `LE.le.trans` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Ideal.absNorm_pos_of_nonZeroDivisors` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `Ideal.absNorm_dvd_absNorm_of_le` `Ideal.le_of_dvd` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors`
`isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc` 📖	mathematical	`Submodule.IsPrincipal` `NumberField.RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`IsPrincipalIdealRing`	—	`Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `NumberField.to_charZero` `isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime` `NumberField.RingOfIntegers.instNontrivial` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `IsPrincipalIdealRing.principal` `EuclideanDomain.to_principal_ideal_domain` `nonZeroDivisors.coe_ne_zero` `Ideal.instNontrivial` `Ideal.eq_bot_of_comap_eq_bot` `Int.instNontrivial` `NumberField.RingOfIntegers.instIsDomain` `NumberField.RingOfIntegers.instIsIntegralInt` `RingHom.instRingHomClass` `Ideal.span_singleton_prime` `abs_choice` `Ideal.over_under` `Nat.cast_natAbs` `Int.cast_neg` `Ideal.span_singleton_neg` `Nat.le_floor` `Real.instIsOrderedRing` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Ideal.absNorm_eq_pow_inertiaDeg` `Module.IsNoetherian.finite` `NumberField.RingOfIntegers.instIsNoetherianInt` `Ideal.IsPrime.under` `Int.prime_iff_natAbs_prime` `Ideal.IsPrime.isMaximal` `IsDedekindDomainDvr.ring_dimensionLEOne` `Int.instIsDomain` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `Ideal.isPrime_of_prime` `Ideal.prime_span_singleton_iff` `Prime.ne_zero` `Ideal.inertiaDeg_pos` `Finset.mem_Icc` `Nat.Prime.one_le` `le_trans`

---

← Back to Index