toCLM_apply_single_apply — Mathlib

English

For DecidableEq m, and a ∈ A, (toCLM M) applied to the basis Pi.single i a yields the map j ↦ a · M_{i j}. Hence the i-th row acts by left multiplication by a.

Русский

Для исхода DecidableEq m и a ∈ A, (toCLM M) применяется к базису Pi.single i a, дает отображение j ↦ a · M_{i j}; значит i-я строка действует слева перемножив на a.

LaTeX

$$(toCLM M)(equiv _ _ |> symm |> Pi.single i a) _ j = a * M_{i j}$$

Lean4

theorem toCLM_apply_single_apply [DecidableEq m] {M : CStarMatrix m n A} {i : m} {j : n} (a : A) :
    (toCLM M) (equiv _ _ |>.symm <| Pi.single i a) j = a * M i j := by simp

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