map_spanIntNorm — Mathlib

English

For any I and f, the equality in map_spanIntNorm holds: map f (spanNorm R I) = span ( image of intNorm through f over I ).

Русский

Для данного I и отображения f выполняется равенство: map f (spanNorm R I) = span (image (intNorm) через f на I).

LaTeX

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

Lean4

theorem map_spanIntNorm (I : Ideal S) {T : Type*} [Semiring T] (f : R →+* T) :
    map f (spanNorm R I) = span (f ∘ Algebra.intNorm R S '' (I : Set S)) :=
  by
  rw [spanNorm]
  nth_rw 2 [map]
  simp [map_span, Set.image_image]

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