adjoin_union_coe_submodule — Mathlib

English

The submodule underlying adjoin of s ∪ t equals the product of the submodules underlying adjoin s and adjoin t.

Русский

Базовый подмодуль подадьюйн-объединения s ∪ t равен произведению подмодулей adjoin s и adjoin t.

LaTeX

$$$\\operatorname{toSubmodule}(\\operatorname{adjoin}_R( s \\cup t)) = \\operatorname{toSubmodule}(\\operatorname{adjoin}_R s) \\; * \\; \\operatorname{toSubmodule}(\\operatorname{adjoin}_R t)$$$

Lean4

theorem adjoin_union_coe_submodule :
    Subalgebra.toSubmodule (adjoin R (s ∪ t)) =
      Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t) :=
  by
  rw [adjoin_eq_span, adjoin_eq_span, adjoin_eq_span, span_mul_span]
  congr 1 with z; simp [Submonoid.closure_union, Submonoid.mem_sup, Set.mem_mul]

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