English
If r ∈ I^n, then the monomial n r belongs to the subalgebra generated by the image of I under the map monomial 1.
Русский
Если r ∈ I^n, то мононом n r принадлежит подалгебре, порождаемой образами элементов I через отображение monomial 1.
LaTeX
$$$\text{monomial } n\, r \in \mathrm{Algebra.adjoin}\, R\big(\mathrm{Submodule.map}(\mathrm{Polynomial.monomial}\, 1)\, I : \text{Set } R[X]\big)$ при условии $r \in I^{n}$$$
Lean4
theorem monomial_mem_adjoin_monomial {I : Ideal R} {n : ℕ} {r : R} (hr : r ∈ I ^ n) :
monomial n r ∈ Algebra.adjoin R (Submodule.map (monomial 1 : R →ₗ[R] R[X]) I : Set R[X]) := by
induction n generalizing r with
| zero => exact Subalgebra.algebraMap_mem _ _
| succ n hn =>
rw [pow_succ'] at hr
refine Submodule.smul_induction_on hr ?_ ?_
· intro r hr s hs
rw [add_comm n 1, smul_eq_mul, ← monomial_mul_monomial]
exact Subalgebra.mul_mem _ (Algebra.subset_adjoin (Set.mem_image_of_mem _ hr)) (hn hs)
· intro x y hx hy
rw [monomial_add]
exact Subalgebra.add_mem _ hx hy
