monomial_one_right_eq_X_pow — Mathlib

English

If R is nontrivial, then the indeterminate X is not equal to any constant polynomial C(a).

Русский

Если R не тривиален, то X не равен никакому константному полиному C(a).

LaTeX

$$$ X \neq C(a) \quad \text{for all } a \in R \text{ when } R \text{ is nontrivial}. $$$

Lean4

theorem monomial_one_right_eq_X_pow (n : ℕ) : monomial n (1 : R) = X ^ n := by
  induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]

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