aeval_apply_smul_mem_of_le_comap — Mathlib

English

A specialized version of the previous lemma: given hm ∈ q, p ∈ R[X], a ∈ A, and hq: q ≤ q.comap (lsmul a), we have aeval a p · m ∈ q.

Русский

Уточненная версия леммы: если hm ∈ q, p ∈ R[X], a ∈ A и hq: q ≤ q.comap (lsmul a), тогда aeval a p · m ∈ q.

LaTeX

$$$ aeval\ a\ p \;\cdot m \in q \quad\text{при } hm:\ m \in q,\ p : R[X],\ a : A,\ hq : q \le q.comap (lsmul R R M a) $$$

Lean4

theorem aeval_apply_smul_mem_of_le_comap (hm : m ∈ q) (p : R[X]) (f : Module.End R M) (hq : q ≤ q.comap f) :
    aeval f p m ∈ q :=
  aeval_apply_smul_mem_of_le_comap' hm p f hq

Похожие утверждения