instIsScalarTowerPolynomial — Mathlib

English

There is a scalar tower structure making Laurent polynomials into a module over R[X] and R[X] acting on them, i.e. the associative law holds: (p q) • z = p • (q • z) for p, q in R[X] and z in R[T; T^{-1}].

Русский

Существует структура каскадного действия скаляров так, что полиномы Лорент образуют модуль над R[X], и выполняется ассоциативность: (pq)⋅z = p⋅(q⋅z) для p, q ∈ R[X] и z ∈ R[T; T^{-1}].

LaTeX

$$$IsScalarTower\\;R[X]\\;R[X]\\;R[T;T^{-1}]$.$$

Lean4

instance (R : Type*) [Semiring R] : IsScalarTower R[X] R[X] R[T;T⁻¹] where
  smul_assoc x y z := by dsimp; simp_rw [MulAction.mul_smul]

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