sumInl — Mathlib

English

Given a TransvectionStruct on n, form a TransvectionStruct on n ⊕ p by embedding on the left (sumInl).

Русский

Пусть данна структура трансвеκции на n; образуем структуру на n ⊕ p, где индексы введены через левое вложение (sumInl).

LaTeX

$$$\\text{sumInl }(p) : \\text{TransvectionStruct }(n\\oplus p)\\,R\\;\\text{defined by } i:=\\mathrm{inl}(t.i),\\; j:=\\mathrm{inl}(t.j),\\; hij:=t.hij,\\; c:=t.c$$$

Lean4

/-- Given a `TransvectionStruct` on `n`, define the corresponding `TransvectionStruct` on `n ⊕ p`
using the identity on `p`. -/
def sumInl (t : TransvectionStruct n R) : TransvectionStruct (n ⊕ p) R
    where
  i := inl t.i
  j := inl t.j
  hij := by simp [t.hij]
  c := t.c

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