expand_monomial — Mathlib

English

Let R be a commutative semiring and p, q be natural numbers with r in R. Expanding the monomial q with coefficient r by p yields the monomial with exponent pq and coefficient r:

Русский

Пусть R — коммутативное полукольцо, p и q — натуральные числа, а r ∈ R. Расширение монома q с коэффициентом r по p даёт мономиал с показателем pq и коэффициентом r:

LaTeX

$$$\operatorname{expand}(R,p)\bigl(\operatorname{monomial}(q,r)\bigr) = \operatorname{monomial}(q p, r)$$$

Lean4

@[simp]
theorem expand_monomial (r : R) : expand R p (monomial q r) = monomial (q * p) r := by
  simp_rw [← smul_X_eq_monomial, map_smul, map_pow, expand_X, mul_comm, pow_mul]

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