Domain

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

Statistics

Metric	Count
Definitions	0
Theorems degree_le_of_dvd, eq_zero_of_dvd_of_degree_lt, eq_zero_of_dvd_of_natDegree_lt, natDegree_le_of_dvd, natDegree_mul, natDegree_pow, natDegree_smul, natDegree_sub_eq_of_prod_eq, not_dvd_of_degree_lt, not_dvd_of_natDegree_lt	10
Total	10

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degree_le_of_dvd 📖	mathematical	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree	—	degree_le_mul_left mul_ne_zero_iff instNoZeroDivisors
eq_zero_of_dvd_of_degree_lt 📖	mathematical	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree	instZero	—	lt_iff_not_ge degree_le_of_dvd
eq_zero_of_dvd_of_natDegree_lt 📖	mathematical	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring natDegree	instZero	—	lt_iff_not_ge natDegree_le_of_dvd
natDegree_le_of_dvd 📖	mathematical	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring	natDegree	—	natDegree_mul mul_ne_zero_iff instNoZeroDivisors
natDegree_mul 📖	mathematical	—	natDegree Polynomial instMul	—	WithBot.charZero Nat.instCharZero degree_eq_natDegree mul_ne_zero instNoZeroDivisors Nat.cast_add degree_mul
natDegree_pow 📖	mathematical	—	natDegree Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	eq_or_ne pow_zero natDegree_one MulZeroClass.mul_zero zero_pow natDegree_pow' leadingCoeff_pow leadingCoeff_eq_zero pow_ne_zero isReduced_of_noZeroDivisors instNoZeroDivisors
natDegree_smul 📖	mathematical	—	natDegree Polynomial SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	smul_zero natDegree_eq_of_le_of_coeff_ne_zero LE.le.trans natDegree_smul_le le_refl coeff_smul smul_ne_zero IsDomain.toIsCancelMulZero
natDegree_sub_eq_of_prod_eq 📖	mathematical	Polynomial instMul	natDegree	—	sub_eq_sub_iff_add_eq_add Int.instCharZero natDegree_mul
not_dvd_of_degree_lt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring	—	eq_zero_of_dvd_of_degree_lt
not_dvd_of_natDegree_lt 📖	mathematical	natDegree	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring	—	eq_zero_of_dvd_of_natDegree_lt

---

← Back to Index