Documentation Verification Report

Degree

📁 Source: Mathlib/FieldTheory/RatFunc/Degree.lean

Statistics

Metric	Count
Definitions `intDegree`	1
Theorems `intDegree_C`, `intDegree_X`, `intDegree_add`, `intDegree_add_le`, `intDegree_div`, `intDegree_inv`, `intDegree_mul`, `intDegree_neg`, `intDegree_one`, `intDegree_polynomial`, `intDegree_zero`, `natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree`	12
Total	13

RatFunc

Definitions

Name	Category	Theorems
`intDegree` 📖	CompOp	14 math math: `intDegree_div`, `FunctionField.inftyValuation_of_nonzero`, `intDegree_inv`, `intDegree_mul`, `intDegree_C`, `intDegree_add_le`, `intDegree_add`, `intDegree_polynomial`, `valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X`, `natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree`, `intDegree_one`, `intDegree_X`, `intDegree_neg`, `intDegree_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intDegree_C` 📖	mathematical	—	`intDegree` `DFunLike.coe` `RingHom` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instIsDomain` `RingHom.instFunLike` `C`	—	`instIsDomain` `intDegree.eq_1` `num_C` `Polynomial.natDegree_C` `denom_C` `Polynomial.natDegree_one` `sub_self`
`intDegree_X` 📖	mathematical	—	`intDegree` `X` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield`	—	`instIsDomain` `intDegree.eq_1` `num_X` `Polynomial.natDegree_X` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `denom_X` `Polynomial.natDegree_one` `sub_zero`
`intDegree_add` 📖	mathematical	—	`intDegree` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instAdd` `Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial` `Polynomial.instAdd` `Polynomial.instMul` `num` `denom`	—	`Polynomial.natDegree_sub_eq_of_prod_eq` `IsDomain.to_noZeroDivisors` `instIsDomain` `num_ne_zero` `denom_ne_zero` `num_mul_denom_add_denom_mul_num_ne_zero` `mul_ne_zero` `Polynomial.instNoZeroDivisors` `num_denom_add`
`intDegree_add_le` 📖	mathematical	—	`intDegree` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instAdd`	—	`zero_add` `instIsDomain` `intDegree_zero` `intDegree_add` `natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree` `denom_ne_zero` `mul_comm` `le_max_iff` `sub_le_sub_iff_right` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `Polynomial.natDegree_add_le`
`intDegree_div` 📖	mathematical	—	`intDegree` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instDiv` `instIsDomain` `Field.toSemifield`	—	`instIsDomain` `div_eq_mul_inv` `intDegree_mul` `intDegree_inv` `sub_eq_add_neg`
`intDegree_inv` 📖	mathematical	—	`intDegree` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instInv` `instIsDomain` `Field.toSemifield`	—	`instIsDomain` `inv_zero` `intDegree_zero` `neg_zero` `intDegree_mul` `inv_ne_zero` `inv_mul_cancel₀` `intDegree_one`
`intDegree_mul` 📖	mathematical	—	`intDegree` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul`	—	`add_sub` `sub_add` `sub_sub_eq_add_sub` `sub_sub` `Int.instCharZero` `Polynomial.natDegree_mul` `IsDomain.to_noZeroDivisors` `instIsDomain` `denom_ne_zero` `num_ne_zero` `mul_ne_zero` `Polynomial.instNoZeroDivisors` `num_denom_mul`
`intDegree_neg` 📖	mathematical	—	`intDegree` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instNeg`	—	`instIsDomain` `neg_zero` `intDegree.eq_1` `Polynomial.natDegree_neg` `Polynomial.natDegree_sub_eq_of_prod_eq` `IsDomain.to_noZeroDivisors` `num_ne_zero` `neg_ne_zero` `denom_ne_zero` `num_denom_neg`
`intDegree_one` 📖	mathematical	—	`intDegree` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instOne`	—	`intDegree.eq_1` `num_one` `denom_one` `sub_self`
`intDegree_polynomial` 📖	mathematical	—	`intDegree` `DFunLike.coe` `RingHom` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Polynomial.commSemiring` `Semifield.toCommSemiring` `instField` `instIsDomain` `RingHom.instFunLike` `algebraMap` `instAlgebraOfPolynomial` `Algebra.id` `Polynomial.natDegree`	—	`instIsDomain` `intDegree.eq_1` `num_algebraMap` `denom_algebraMap` `Polynomial.natDegree_one` `sub_zero`
`intDegree_zero` 📖	mathematical	—	`intDegree` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instZero`	—	`intDegree.eq_1` `num_zero` `Polynomial.natDegree_zero` `denom_zero` `Polynomial.natDegree_one` `sub_self`
`natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree` 📖	mathematical	—	`Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial` `Polynomial.instMul` `num` `denom` `intDegree`	—	`Polynomial.natDegree_sub_eq_of_prod_eq` `IsDomain.to_noZeroDivisors` `instIsDomain` `mul_ne_zero` `Polynomial.instNoZeroDivisors` `num_ne_zero` `denom_ne_zero` `mul_assoc`

---

← Back to Index