Documentation Verification Report

AdmissibleCardPowDegree

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

Statistics

Metric	Count
Definitions `cardPowDegreeIsAdmissible`	1
Theorems `cardPowDegree_anti_archimedean`, `exists_approx_polynomial`, `exists_approx_polynomial_aux`, `exists_eq_polynomial`, `exists_partition_polynomial`, `exists_partition_polynomial_aux`	6
Total	7

Polynomial

Definitions

Name	Category	Theorems
`cardPowDegreeIsAdmissible` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardPowDegree_anti_archimedean` 📖	mathematical	`DFunLike.coe` `AbsoluteValue` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semiring` `Int.instSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `AbsoluteValue.funLike` `cardPowDegree` `instSub` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `AbsoluteValue` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semiring` `Int.instSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `AbsoluteValue.funLike` `cardPowDegree` `instSub` `DivisionRing.toRing` `Field.toDivisionRing`	—	`lt_of_le_of_lt` `AbsoluteValue.nonneg` `sub_self` `map_zero` `AbsoluteValue.zeroHomClass` `cardPowDegree_nonzero` `sub_ne_zero` `Nat.cast_one` `Int.instAddLeftMono` `Int.instZeroLEOneClass` `Int.instCharZero` `LT.lt.le` `Fintype.one_lt_card` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `pow_le_pow_right₀` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `natDegree_le_iff_degree_le` `le_max_iff` `degree_eq_natDegree` `sub_add_sub_cancel` `degree_add_le` `max_lt`
`exists_approx_polynomial` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Monoid.toPow` `Nat.instMonoid` `Fintype.card` `Nat.ceil` `Real` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNeg` `Real.log` `Real.instNatCast` `Real.instLT` `Real.instIntCast` `DFunLike.coe` `AbsoluteValue` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semiring` `Int.instSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `AbsoluteValue.funLike` `cardPowDegree` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `instMod` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `Real.instAddGroup`	—	`Real.instIsStrictOrderedRing` `Algebra.smul_def` `eq_intCast` `RingHom.instRingHomClass` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Int.cast_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `AbsoluteValue.pos` `Fintype.one_lt_card` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Nat.cast_one` `Nat.cast_zero` `exists_eq_polynomial` `le_rfl` `EuclideanDomain.mod_lt` `sub_self` `map_zero` `AbsoluteValue.zeroHomClass` `Int.cast_zero` `exists_approx_polynomial_aux` `sub_eq_zero` `lt_of_lt_of_le` `Nat.cast_lt` `WithBot.coe_lt_coe` `degree_eq_natDegree` `sub_neg_eq_add` `neg_div` `Nat.cast_sub` `LT.lt.le` `le_imp_le_of_le_of_le` `sub_le_sub_left` `covariant_swap_add_of_covariant_add` `Nat.le_ceil` `le_refl` `Real.log_lt_log_iff` `cardPowDegree_nonzero` `Int.cast_pow` `Int.cast_natCast` `Real.log_mul` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `LT.lt.ne'` `Real.rpow_natCast` `Real.log_rpow` `lt_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.log_pos` `add_div` `mul_div_cancel_right₀` `EuclideanDomain.toMulDivCancelClass`
`exists_approx_polynomial_aux` 📖	mathematical	`Monoid.toPow` `Nat.instMonoid` `Fintype.card` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Ring.toSemiring`	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Ring.toSemiring` `Polynomial` `instSub` `WithBot.natCast` `natDegree`	—	`not_lt_of_ge` `bot_le` `degree_zero` `Fintype.card_pi` `Finset.prod_const` `Fintype.card_fin` `Nat.instNoMaxOrder` `lt_of_le_of_lt` `Fintype.exists_ne_map_eq_of_card_lt` `degree_lt_iff_coeff_zero` `coeff_eq_zero_of_degree_lt` `lt_of_lt_of_le` `degree_sub_le` `max_lt` `coeff_sub` `sub_eq_zero` `WithBot.coe_lt_coe` `degree_eq_natDegree` `tsub_le_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `tsub_lt_iff_tsub_lt` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `tsub_tsub_cancel_of_le` `LT.lt.le`
`exists_eq_polynomial` 📖	—	`Monoid.toPow` `Nat.instMonoid` `Fintype.card` `natDegree` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	—	—	`Fintype.card_pi` `Finset.prod_const` `Fintype.card_fin` `Nat.instNoMaxOrder` `lt_of_le_of_lt` `Fintype.exists_ne_map_eq_of_card_lt` `ext` `coeff_eq_zero_of_degree_lt` `lt_of_lt_of_le` `coe_lt_degree`
`exists_partition_polynomial` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real` `Real.instLT` `Real.instIntCast` `DFunLike.coe` `AbsoluteValue` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semiring` `Int.instSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `AbsoluteValue.funLike` `cardPowDegree` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `instMod` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `Real.instAddGroup`	—	`Real.instIsStrictOrderedRing` `exists_partition_polynomial_aux`
`exists_partition_polynomial_aux` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real` `Real.instLT` `Real.instIntCast` `DFunLike.coe` `AbsoluteValue` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semiring` `Int.instSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `AbsoluteValue.funLike` `cardPowDegree` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `instMod` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `Real.instAddGroup`	—	`Algebra.smul_def` `eq_intCast` `RingHom.instRingHomClass` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Int.cast_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `AbsoluteValue.pos` `cardPowDegree_anti_archimedean` `Mathlib.Tactic.Push.not_forall_eq` `exists_approx_polynomial` `AbsoluteValue.map_sub` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `NormMulClass.toNoZeroDivisors` `Int.instNormMulClass` `not_le` `Fin.cons_zero` `Fin.cons_succ` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `sub_self` `AbsoluteValue.map_zero` `Int.cast_zero` `zsmul_eq_mul`

---

← Back to Index