eq_of_isLocalized'_span — Mathlib

English

If all localized images of N are top, then N is top.

Русский

Если все локализованные изображения N равны вершинe, то N равен вершине.

LaTeX

$$$$\forall r, N localized' (R_p r) powers r.top = M top \Rightarrow N = M top.$$$$

Lean4

theorem eq_of_isLocalized'_span {N P : Submodule R M}
    (h : ∀ r, N.localized' (Rₚ r) (.powers r.1) (f r) = P.localized' (Rₚ r) (.powers r.1) (f r)) : N = P :=
  eq_of_isLocalized₀_span s span_eq _ f fun r ↦ congr(restrictScalars _ $(h r))

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