smul_basis_mul_C — Mathlib

English

Relates the smul-basis expression with the generator Y in the coordinate ring basis, showing how mk W' Y interacts with polynomials p, q.

Русский

Связывает выражение smul-базы с генератором Y в базе координатного кольца, показывая взаимодействие mk W' Y с полиномами p, q.

LaTeX

$$(p • (1 : W'.CoordinateRing) + q • mk W' Y) • mk W' Y = (q * (X^3 + C W'.a₂ X^2 + C W'.a₄ X + C W'.a₆)) • (1 : W'.CoordinateRing) + (p - q * (C W'.a₁ X + C W'.a₃)) • mk W' Y$$

Lean4

theorem smul_basis_mul_C (y : R[X]) (p q : R[X]) :
    (p • (1 : W'.CoordinateRing) + q • mk W' Y) * mk W' (C y) = (p * y) • (1 : W'.CoordinateRing) + (q * y) • mk W' Y :=
  by
  simp only [smul, map_mul]
  ring1

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