SeparableDegree

📁 Source: Mathlib/RingTheory/Polynomial/SeparableDegree.lean

Statistics

Metric	Count
Definitions HasSeparableContraction, contraction, degree, IsSeparableContraction	4
Theorems hasSeparableContraction, dvd_degree, dvd_degree', eq_degree, isSeparableContraction, degree_eq, dvd_degree', contraction_degree_eq_or_insep	8
Total	12

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasSeparableContraction 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.HasSeparableContraction Semifield.toCommSemiring	—	separable pow_zero Polynomial.expand_one Polynomial.exists_separable_of_irreducible Nat.Prime.ne_zero

Polynomial

Definitions

Name	Category	Theorems
HasSeparableContraction 📖	MathDef	1 math math: Irreducible.hasSeparableContraction
IsSeparableContraction 📖	MathDef	1 math math: HasSeparableContraction.isSeparableContraction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contraction_degree_eq_or_insep 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toNatPow Nat.instMonoid Separable	natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd isUnit_or_eq_zero_of_separable_expand NeZero.pos natDegree_expand natDegree_eq_zero_of_isUnit IsDomain.to_noZeroDivisors instIsDomain MulZeroClass.zero_mul pow_zero mul_one pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass expand_mul pow_add le_of_not_ge

Polynomial.HasSeparableContraction

Definitions

Name	Category	Theorems
contraction 📖	CompOp	1 math math: isSeparableContraction
degree 📖	CompOp	5 math math: dvd_degree, natSepDegree_eq, eq_degree, dvd_degree', Polynomial.IsSeparableContraction.degree_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_degree 📖	mathematical	Polynomial.HasSeparableContraction	degree Polynomial.natDegree CommSemiring.toSemiring	—	dvd_degree' Dvd.intro
dvd_degree' 📖	mathematical	Polynomial.HasSeparableContraction	degree Monoid.toNatPow Nat.instMonoid Polynomial.natDegree CommSemiring.toSemiring	—	Polynomial.IsSeparableContraction.dvd_degree'
eq_degree 📖	mathematical	Polynomial.HasSeparableContraction	degree Polynomial.natDegree CommSemiring.toSemiring	—	dvd_degree' one_pow mul_one
isSeparableContraction 📖	mathematical	Polynomial.HasSeparableContraction	Polynomial.IsSeparableContraction contraction	—	—

Polynomial.IsSeparableContraction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degree_eq 📖	mathematical	Polynomial.HasSeparableContraction Semifield.toCommSemiring Field.toSemifield Polynomial.IsSeparableContraction	Polynomial.natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.HasSeparableContraction.degree	—	Polynomial.HasSeparableContraction.eq_degree Polynomial.expand_one one_pow Polynomial.contraction_degree_eq_or_insep NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt'
dvd_degree' 📖	mathematical	Polynomial.IsSeparableContraction	Polynomial.natDegree CommSemiring.toSemiring Monoid.toNatPow Nat.instMonoid	—	Polynomial.natDegree_expand

---

← Back to Index