rootSpanMem — Mathlib

English

There is a canonical embedding of a root as an element of the root span: rootSpanMem i ∈ P.rootSpan S.

Русский

Существует каноническое вложение корня в корневую область: rootSpanMem i ∈ P.rootSpan S.

LaTeX

$$$rootSpanMem\;S\;i \in P.rootSpan S$$$

Lean4

/-- A root, seen as an element of the span of roots. -/
abbrev rootSpanMem [Module S M] (i : ι) : P.rootSpan S :=
  ⟨P.root i, Submodule.subset_span (mem_range_self i)⟩

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