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 📖	—	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	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.toNatPow Nat.instMonoid Fintype.card WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree Ring.toSemiring	Polynomial instSub AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne 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 AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le tsub_tsub_cancel_of_le LT.lt.le
exists_eq_polynomial 📖	—	Monoid.toNatPow 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.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.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