IsIntegral

Statistics

Metric	Count
Definitions	0
Theorems `isIntegral_int_I`, `isIntegral_rat_I`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegral_int_I` 📖	mathematical	—	`IsIntegral` `Complex` `Int.instCommRing` `instRing` `Ring.toIntAlgebra` `I`	—	`Polynomial.monic_X_pow_add_C` `two_ne_zero` `Polynomial.eval₂_add` `Polynomial.eval₂_X_pow` `Polynomial.eval₂_C` `I_sq` `eq_intCast` `RingHom.instRingHomClass` `Int.cast_one` `neg_add_cancel`
`isIntegral_rat_I` 📖	mathematical	—	`IsIntegral` `Complex` `Rat.commRing` `instRing` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `instField` `instCharZero` `I`	—	`IsIntegral.tower_top` `instCharZero` `AddCommGroup.intIsScalarTower` `isIntegral_int_I`

---