spanNorm_singleton — Mathlib

English

If x ∈ I, then Algebra.intNorm R S x ∈ I.spanNorm R.

Русский

Если x ∈ I, то Algebra.intNorm(R,S)(x) ∈ I.spanNorm.

LaTeX

$$$$\operatorname{intNorm}(R,S)(x) \in \operatorname{spanNorm}(R,I) \text{ whenever } x\in I.$$$$

Lean4

@[simp]
theorem spanNorm_singleton {r : S} : spanNorm R (span ({ r } : Set S)) = span {Algebra.intNorm R S r} :=
  le_antisymm
    (span_le.mpr fun x hx =>
      mem_span_singleton.mpr
        (by
          obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx
          exact map_dvd _ (mem_span_singleton.mp hx')))
    ((span_singleton_le_iff_mem _).mpr (intNorm_mem_spanNorm _ (mem_span_singleton_self _)))

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