mem_toNonUnitalSubalgebra — Mathlib

English

x ∈ p.toNonUnitalSubalgebra hmul ↔ x ∈ p; the carrier is unchanged when passing from a submodule to the corresponding nonunital subalgebra.

Русский

Членство x в p.toNonUnitalSubalgebra hmul эквивалентно членству x в p; носитель не меняется при переходе от подмодуля к соответствующей немонолитной подалгебре.

LaTeX

$$$x \\in p^{\\mathrm{toNonUnitalSubalgebra}}_{hmul} \\iff x \\in p$$$

Lean4

@[simp]
theorem mem_toNonUnitalSubalgebra {p : Submodule R A} {h_mul} {x} : x ∈ p.toNonUnitalSubalgebra h_mul ↔ x ∈ p :=
  Iff.rfl

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