C_pow

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.C_pow

English

Constant powers pass through C: C(a^n) = (C a)^n.

Русский

Степени констант проходят через C: C(a^n) = (C a)^n.

LaTeX

$$$ C\ (a ^ n) = (C\ a) ^ n $$$

Lean4

@[simp]
theorem C_pow (a : R) (n : ℕ) : (C (a ^ n) : MvPolynomial σ R) = C a ^ n :=
  map_pow _ _ _

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

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

Разделы

Аффилиация

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