relNorm_singleton — Mathlib

English

For any ring hom f : R → T, relNorm(f(I)) = span image of intNorm under f: map f (relNorm_R I) = span( f ∘ intNorm_R_S '' I ).

Русский

Для гомоморфизма f: R → T выполняется: relNorm(f(I)) = span( f( intNorm_R_S(I) ) ).

LaTeX

$$$\mathrm{map}_f(\mathrm{relNorm}_R(I)) = \operatorname{span}\big( f \circ \mathrm{intNorm}_{R,S} \big[ I \big] \big).$$$

Lean4

@[simp]
theorem relNorm_singleton (r : S) : relNorm R (span ({ r } : Set S)) = span {Algebra.intNorm R S r} :=
  spanNorm_singleton R

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