baseChange_top — Mathlib

English

Base-change of the top submodule is top: (⊤ : Submodule_R M).baseChange A = ⊤.

Русский

Расширение топ-подмодуля даёт топ: (⊤ : Submodule_R M).baseChange A = ⊤.

LaTeX

$$$$ (\\top) baseChange A = \\top. $$$$

Lean4

@[simp]
theorem baseChange_top : (⊤ : Submodule R M).baseChange A = ⊤ :=
  by
  rw [eq_top_iff, ← span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..)]
  exact span_le.2 fun _ ⟨a, m, h⟩ ↦ h ▸ tmul_mem_baseChange_of_mem _ trivial

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