instIsScalarTowerOrigPolynomial — Mathlib

English

Higher powers of X act on AEval via the corresponding powers of a.

Русский

Степени X действуют на AEval соответствующими степенями a.

LaTeX

$$$ (X^n : R[X]) \\cdot (of\\ R\\ M\\ a\\ m) = of\\ R\\ M\\ a (a^n \\cdot m) $$$

Lean4

instance instIsScalarTowerOrigPolynomial : IsScalarTower R R[X] <| AEval R M a where
  smul_assoc r f
    m := by
    apply (of R M a).symm.injective
    rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]

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