Theorem Polynomial.aeval_algebraMap_eq_zero_iff

Modification history

2026-01-13 19:40
Mathlib/RingTheory/Polynomial/Tower.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified Polynomial.aeval_algebraMap_eq_zero_iffView on Github →
2023-03-13 14:02
Mathlib/RingTheory/Polynomial/Tower.lean
feat: Port RingTheory.Polynomial.Tower (#2840) …
Added Polynomial.aeval_algebraMap_eq_zero_iffView on Github →