adjoin_X — Mathlib

English

The subalgebra generated by the indeterminate X inside the polynomial ring equals the top subalgebra: adjoin_R({X}) = ⊤.

Русский

Подалгебра, порождаемая независимой переменной X в кольце многочленов, равна верхнему подалгебре: adjoin_R({X}) = ⊤.

LaTeX

$$$\\operatorname{adjoin}_R(\\{X\\}) = \\top$$$

Lean4

@[simp]
theorem adjoin_X : adjoin R ({ X } : Set R[X]) = ⊤ :=
  by
  refine top_unique fun p _hp => ?_
  set S := adjoin R ({ X } : Set R[X])
  rw [← sum_monomial_eq p]; simp only [← smul_X_eq_monomial]
  exact S.sum_mem fun n _hn => S.smul_mem (S.pow_mem (subset_adjoin rfl) _) _

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