mem_range_scalar_of_commute_transvectionStruct

English

A variant form of the previous identities: the product of inverses taken in reverse order multiplies with the forward product to yield the identity.

Русский

Вариант формы предыдущих тождеств: произведение обратных в обратном порядке умножения даёт идентичность с прямым произведением.

LaTeX

$$$\\Big(\\prod_{t\\in L^{\\mathrm{rev}}} t.inv.toMatrix\\Big) \\cdot \\Big(\\prod_{t\\in L} t.toMatrix\\Big) = 1$$$

Lean4

/-- `M` is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix). -/
theorem _root_.Matrix.mem_range_scalar_of_commute_transvectionStruct {M : Matrix n n R}
    (hM : ∀ t : TransvectionStruct n R, Commute t.toMatrix M) : M ∈ Set.range (Matrix.scalar n) :=
  by
  refine mem_range_scalar_of_commute_single ?_
  intro i j hij
  simpa [transvection, mul_add, add_mul] using (hM ⟨i, j, hij, 1⟩).eq

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