Documentation Verification Report

IntPolynomial

📁 Source: Mathlib/Algebra/Ring/Subring/IntPolynomial.lean

Statistics

Metric	Count
Definitions `int`	1
Theorems `int_coeff_eq`, `int_eval₂_eq`, `int_leadingCoeff_eq`, `int_monic_iff`, `int_natDegree`	5
Total	6

Polynomial

Definitions

Name	Category	Theorems
`int` 📖	CompOp	5 math math: `int_coeff_eq`, `int_eval₂_eq`, `int_leadingCoeff_eq`, `int_monic_iff`, `int_natDegree`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`int_coeff_eq` 📖	mathematical	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `coeff` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `int`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass`
`int_eval₂_eq` 📖	mathematical	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `coeff` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`eval₂` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `algebraMap` `Algebra.ofSubring` `Field.toCommRing` `int` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `aeval_eq_sum_range` `eval₂_eq_sum_range` `Finset.sum_congr` `Algebra.smul_def`
`int_leadingCoeff_eq` 📖	mathematical	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `coeff` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`leadingCoeff` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `int`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass`
`int_monic_iff` 📖	mathematical	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `coeff` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Monic` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `int`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Monic.eq_1` `int_leadingCoeff_eq` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `OneMemClass.coe_eq_one`
`int_natDegree` 📖	mathematical	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `coeff` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`natDegree` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `int`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass`

---

← Back to Index