monic_geom_sum_X — Mathlib

English

For P monic with positive degree, the partial geometric sum (P^0 + P^1 + ... + P^{n-1}) is monic for n ≠ 0.

Русский

Для монического P с положительной степенью, частичная геометрическая сумма (P^0 + P^1 + ... + P^{n-1}) моническое при n ≠ 0.

LaTeX

$$$P\text{ мон.} \land 0<\deg P \Rightarrow \bigl(\sum_{i=0}^{n-1} P^i\bigr)\text{Monic}$, при $n\neq0$.$$

Lean4

theorem monic_geom_sum_X {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ range n, (X : R[X]) ^ i).Monic :=
  by
  nontriviality R
  apply monic_X.geom_sum _ hn
  simp only [natDegree_X, zero_lt_one]

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