intNorm_mem_spanNorm — Mathlib

English

For any I ∈ Ideal S and any ring hom f: R →+* T, the image of spanNorm R I under f equals the span of the image of intNorm across I.

Русский

Для любого I ∈ Ideal(S) и гомоморфизма f: R →+* T выполняется равенство: map f (spanNorm R I) = span (f ∘ Algebra.intNorm R S '' I).

LaTeX

$$$$\operatorname{map}(f, \operatorname{spanNorm}(R,I)) = \operatorname{span}\big( f\circ \operatorname{Algebra.intNorm}(R,S)\big''(I) \big).$$$$

Lean4

theorem intNorm_mem_spanNorm {I : Ideal S} {x : S} (hx : x ∈ I) : Algebra.intNorm R S x ∈ I.spanNorm R :=
  subset_span (Set.mem_image_of_mem _ hx)

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