toNonUnitalSubalgebra_mk — Mathlib

English

From a submodule p and a closure hmul, the induced nonunital subalgebra is exactly the explicit construction built from p with the given closure property.

Русский

Из подмодуля p и замыкания hmul получаемая немонолитная подалгебра совпадает с явной конструкцией, построенной на p с заданным свойством замыкания.

LaTeX

$$$p^{\\mathrm{toNonUnitalSubalgebra}}_{hmul} = \\mathrm{NonUnitalSubalgebra.mk}\\left(\\langle\\langle p, p.add\\_mem\\rangle, p.zero\\_mem\\rangle, hmul, p.smul\\_mem'\\right)$$$

Lean4

theorem toNonUnitalSubalgebra_mk (p : Submodule R A) hmul :
    p.toNonUnitalSubalgebra hmul = NonUnitalSubalgebra.mk ⟨⟨⟨p, p.add_mem⟩, p.zero_mem⟩, hmul _ _⟩ p.smul_mem' :=
  rfl

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