nonUnitalSubalgebraOfNonUnitalSubring

English

Let S be a nonunital subring of R. Then there is a nonunital ℤ-subalgebra of R whose underlying nonunital subsemiring is S, with the ℤ-action given by zsmul_mem.

Русский

Пусть S — неединичная подпольга R. Тогда существует неединичная ℤ-подалгебра над R, носитель которой равен S, а действие ℤ задаётся через zsmul_mem.

LaTeX

$$$\\text{Given } S:\\mathrm{NonUnitalSubring}(R),\\ \\operatorname{nonUnitalSubalgebraOfNonUnitalSubring}(S)\\text{ is a nonunital }\\mathbb{Z}\\text{-subalgebra with underlying }S\\text{ and } z\\text{-smul on }S,$$$

Lean4

/-- A non-unital subring is a non-unital `ℤ`-subalgebra. -/
def nonUnitalSubalgebraOfNonUnitalSubring (S : NonUnitalSubring R) : NonUnitalSubalgebra ℤ R
    where
  toNonUnitalSubsemiring := S.toNonUnitalSubsemiring
  smul_mem' n _x hx := zsmul_mem (K := S) hx n

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