inclusion — Mathlib

English

For any S ⊆ A, the range of the valuation map S.val is S.

Русский

Для любой подгруппы S ⊆ A образ отображения S.val есть S.

LaTeX

$$$\text{range}(S.\mathrm{val}) = S$$$

Lean4

/-- The map `S → T` when `S` is a subalgebra contained in the subalgebra `T`.

This is the subalgebra version of `Submodule.inclusion`, or `Subring.inclusion` -/
def inclusion {S T : Subalgebra R A} (h : S ≤ T) : S →ₐ[R] T
    where
  toFun := Set.inclusion h
  map_one' := rfl
  map_add' _ _ := rfl
  map_mul' _ _ := rfl
  map_zero' := rfl
  commutes' _ := rfl

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