monomial_pow — Mathlib

English

For any monomial with exponent vector s and coefficient a in R, and any natural number e, raising the monomial to the e-th power yields the monomial with exponent e • s and coefficient a^e.

Русский

Пусть у monomial с вектором степени s и коэффициентом a в кольце R, и пусть e — натуральное число. Тогда (monomial s a)^e = monomial (e • s) (a^e).

LaTeX

$$$\mathrm{monomial}(s,a)^e = \mathrm{monomial}(e \cdot s, a^e)$$$

Lean4

theorem monomial_pow : monomial s a ^ e = monomial (e • s) (a ^ e) :=
  AddMonoidAlgebra.single_pow ..

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