toSubalgebra — Mathlib

English

A submodule p of A that contains 1 and is closed under multiplication can be upgraded to a subalgebra of A.

Русский

Подмодуль p A, содержащий 1 и замкнутый относительно умножения, может быть преобразован в подалгебру A.

LaTeX

$$$p\toSubalgebra\; (h_1,h_{mul})$$

Lean4

/-- A submodule containing `1` and closed under multiplication is a subalgebra. -/
@[simps coe toSubsemiring]
def toSubalgebra (p : Submodule R A) (h_one : (1 : A) ∈ p) (h_mul : ∀ x y, x ∈ p → y ∈ p → x * y ∈ p) :
    Subalgebra R A :=
  { p with
    mul_mem' := fun hx hy ↦ h_mul _ _ hx hy
    one_mem' := h_one
    algebraMap_mem' := fun r => by
      rw [Algebra.algebraMap_eq_smul_one]
      exact p.smul_mem _ h_one }

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