swap_monomial_monomial

Mathlib.Algebra.Polynomial.Bivariate

URI: https://scilib.ai/kg/mathlib#Polynomial.Bivariate.swap_monomial_monomial

← MathLib Explorer

English

The swap map sends a monomial r X^n Y^m to r X^m Y^n, i.e., it interchanges the exponents of X and Y.

Русский

Обмен переменных переводит многочленный мономиал r X^n Y^m в r X^m Y^n.

LaTeX

$$$swap(r\\,X^n Y^m) = r\\,X^m Y^n.$$$

Lean4

theorem swap_monomial_monomial (n m : ℕ) (r : R) : swap (monomial n (monomial m r)) = (monomial m (monomial n r)) := by
  simp [← C_mul_X_pow_eq_monomial]; ac_rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru