hasBasis_right_ideal — Mathlib

English

If M is a module over R with a linear topology on the left, then the right action basis can be described via right ideals.

Русский

Если M — модуль над R с линейной топологией слева, база правых действий описывается через правые идеалы.

LaTeX

$$$ (\\mathcal{N}0).HasBasis (I : Submodule R^op R \\mapsto (I:Set R) \\in 𝓝 0) (I:Set R) $$$

Lean4

theorem hasBasis_right_ideal [IsLinearTopology Rᵐᵒᵖ R] :
    (𝓝 0).HasBasis (fun I : Submodule Rᵐᵒᵖ R ↦ (I : Set R) ∈ 𝓝 0) (fun I ↦ (I : Set R)) :=
  hasBasis_submodule Rᵐᵒᵖ

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