eq_bot_of_isLocalized₀_span — Mathlib

English

If all localized submodules coincide after restricting scalars, then the underlying submodules agree.

Русский

Если все локализованные подмодули совпадают после редикции скаляров, то сами подмодули совпадают.

LaTeX

$$$$\forall P\,[P^{{\mathrm{Max}}}],\; N localized'^{(R_p P)} = P localized'^{(R_p P)} \Rightarrow N = P.$$$$

Lean4

theorem eq_bot_of_isLocalized₀_span {N : Submodule R M} (h : ∀ r : s, N.localized₀ (.powers r.1) (f r) = ⊥) : N = ⊥ :=
  eq_of_isLocalized₀_span s span_eq Mₚ f fun _ ↦ by simp only [h, Submodule.localized₀_bot]

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