inv — Mathlib

English

The inverse of a TransvectionStruct t is another TransvectionStruct with the same i, j, hij and with coefficient c negated: t.inv has c := -t.c.

Русский

Обратная трансвеκция имеет те же i, j, hij и коэффициент, равный минусу: c := -c.

LaTeX

$$$t^{-1} = \\text{TransvectionStruct}(i,j,hij, -c)$$$

Lean4

/-- The inverse of a `TransvectionStruct`, designed so that `t.inv.toMatrix` is the inverse of
`t.toMatrix`. -/
@[simps]
protected def inv (t : TransvectionStruct n R) : TransvectionStruct n R
    where
  i := t.i
  j := t.j
  hij := t.hij
  c := -t.c

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