snd_invOf — Mathlib

English

If x is invertible and fst(x) is invertible, then the snd-component of the inverse is the negative of a certain mixed smul expression in x.snd and the inverse of x.fst.

Русский

Если x обратим и fst(x) обратимо, то snd(inv x) равна минусу определённого сочетания x.snd и inv fst.

LaTeX

$$$ (inv x).snd = - (inv fst x) \\cdot x.snd $$$

Lean4

theorem snd_invOf (x : tsze R M) [Invertible x] [Invertible x.fst] : (⅟x).snd = -(⅟x.fst •> x.snd <• ⅟x.fst) :=
  by
  letI := invertibleOfInvertibleFst x
  convert congr_arg (TrivSqZeroExt.snd (R := R) (M := M)) (_ : _ = ⅟x)
  convert rfl

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