adjoin_toSubmodule — Mathlib

English

The underlying submodule of the adjoin of s equals the span of the closure of s under nonunital subsemiring operations.

Русский

Грубия underlying-подмодуль ∂ определяется как порожденный через span образ решётки замыкания множества s по операциям негум-неподмодуля.

LaTeX

$$$\operatorname{adjoin}_R(s).toSubmodule = \operatorname{span}_R\bigl( \operatorname{NonUnitalSubsemiring.closure}(s) : Set A \bigr)$$$

Lean4

theorem adjoin_toSubmodule (s : Set A) :
    (adjoin R s).toSubmodule = Submodule.span R (NonUnitalSubsemiring.closure s : Set A) :=
  rfl

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