Theorem Polynomial.aeval_apply_smul_mem_of_le_comap'

Modification history

2024-01-16 21:01
Mathlib/Data/Polynomial/AlgebraMap.lean
feat: basic theory connecting `R[X]`-submodules and invariant `R`-submodules (#9721)
Added Polynomial.aeval_apply_smul_mem_of_le_comap'View on Github →