localized'_top — Mathlib

English

Localization of the top submodule to localized' equals top in the target submodule.

Русский

Локализация верхнего элемента в localized' эквивалентна верхнему элементу в целевом подмодуле.

LaTeX

$$$\\operatorname{localized}'(S,p,f)\\,\\top = \\top.$$$

Lean4

@[simp]
theorem localized'_top : (⊤ : Submodule R M).localized' S p f = ⊤ :=
  SetLike.ext' (by apply SetLike.ext'_iff.mp <| Submodule.localized₀_top p f)

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