toSubalgebra_mk — Mathlib

English

Given a submodule s and proofs of 1 ∈ s and closure under multiplication, s.toSubalgebra h1 hmul equals the Subalgebra constructed from s with the induced multiplication.

Русский

При задании подмодуля s и доказательств того, что 1 ∈ s и замкнутость по умножению, s.toSubalgebra h1 hmul равна подалгебре, построенной на основе s с индуцированным умножением.

LaTeX

$$$s^{toSubalgebra}(h_1,h_{mul}) = \text{Subalgebra built from } s$$$

Lean4

theorem toSubalgebra_mk (s : Submodule R A) (h1 hmul) :
    s.toSubalgebra h1 hmul =
      Subalgebra.mk ⟨⟨⟨s, @hmul⟩, h1⟩, s.add_mem, s.zero_mem⟩
        (by intro r; rw [Algebra.algebraMap_eq_smul_one]; apply s.smul_mem _ h1) :=
  rfl

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