CardPowDegree

📁 Source: Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean

Statistics

Metric	Count
Definitions cardPowDegree	1
Theorems cardPowDegree_apply, cardPowDegree_isEuclidean, cardPowDegree_nonzero, cardPowDegree_zero	4
Total	5

Polynomial

Definitions

Name	Category	Theorems
cardPowDegree 📖	CompOp	7 math math: cardPowDegree_zero, exists_partition_polynomial, exists_partition_polynomial_aux, cardPowDegree_isEuclidean, cardPowDegree_apply, exists_approx_polynomial, cardPowDegree_nonzero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardPowDegree_apply 📖	mathematical	—	DFunLike.coe AbsoluteValue Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semiring Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AbsoluteValue.funLike cardPowDegree instZero instDecidableEq Monoid.toNatPow Int.instMonoid Fintype.card natDegree	—	—
cardPowDegree_isEuclidean 📖	mathematical	—	AbsoluteValue.IsEuclidean Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instEuclideanDomain Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt cardPowDegree	—	Fintype.card_pos_iff Nontrivial.to_nonempty IsSimpleRing.instNontrivial DivisionRing.isSimpleRing pow_pos IsStrictOrderedRing.toPosMulStrictMono Int.instIsStrictOrderedRing Int.instZeroLEOneClass cardPowDegree_apply LT.lt.not_gt degree_eq_natDegree Nat.cast_lt WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero pow_lt_pow_iff_right₀ Nat.cast_one Int.instAddLeftMono Int.instCharZero Fintype.one_lt_card
cardPowDegree_nonzero 📖	mathematical	—	DFunLike.coe AbsoluteValue Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semiring Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AbsoluteValue.funLike cardPowDegree Monoid.toNatPow Int.instMonoid Fintype.card natDegree	—	—
cardPowDegree_zero 📖	mathematical	—	DFunLike.coe AbsoluteValue Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semiring Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AbsoluteValue.funLike cardPowDegree instZero	—	—

---

← Back to Index