mem_bot — Mathlib

English

The bottom subalgebra corresponds, under the toSubmodule map, to the bottom submodule.

Русский

Нижняя подпалгебра переходит в нижний подподмодуль через отображение toSubmodule.

LaTeX

$$$ (\\bot : \\mathrm{NonUnitalSubalgebra}\\, R\\, A).toSubmodule = \\bot $$$

Lean4

theorem mem_bot {x : A} : x ∈ (⊥ : NonUnitalSubalgebra R A) ↔ x = 0 :=
  show x ∈ Submodule.span R (NonUnitalSubsemiring.closure (∅ : Set A) : Set A) ↔ x = 0 by
    rw [NonUnitalSubsemiring.closure_empty, NonUnitalSubsemiring.coe_bot, Submodule.span_zero_singleton,
      Submodule.mem_bot]

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