FiniteDimensional

Statistics

Metric	Count
Definitions	0
Theorems `isTorsion_of_aeval_eq_zero`, `isTorsion_of_finiteDimensional`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`isTorsion_of_aeval_eq_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Module.IsTorsion` `Module.AEval` `instAddCommMonoid` `instModulePolynomial`	—	`mem_nonZeroDivisors_iff_right` `mul_eq_zero` `Polynomial.instNoZeroDivisors` `LinearEquiv.injective` `RingHomInvPair.ids` `zero_smul` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`isTorsion_of_finiteDimensional` 📖	mathematical	—	`Module.IsTorsion` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.AEval` `Semifield.toCommSemiring` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Polynomial.semiring` `instAddCommMonoid` `instModulePolynomial`	—	`isTorsion_of_aeval_eq_zero` `IsDomain.to_noZeroDivisors` `instIsDomain` `minpoly.aeval` `minpoly.ne_zero_of_finite`

---