liftLinear_single — Mathlib

English

Any finite matrix x ∈ Matrix m n α can be written as the finite sum of single i j (x_{i j}) over all i ∈ m, j ∈ n.

Русский

Любую конечную матрицу x ∈ Matrix m n α можно разложить как конечную сумму по всем i ∈ m, j ∈ n: x = ∑_{i,j} single_{i j}(x_{i j}).

LaTeX

$$$ x = \sum_{i \in m} \sum_{j \in n} \mathrm{single}_{i j} (x_{i j}) $$$

Lean4

@[simp]
theorem liftLinear_single (f : m → n → α →ₗ[R] β) (i : m) (j : n) (a : α) :
    liftLinear S f (Matrix.single i j a) = f i j a :=
  by
  dsimp [liftLinear, -LinearMap.lsum_apply, LinearEquiv.congrLeft, LinearEquiv.piCongrRight]
  simp_rw [of_symm_single, LinearMap.lsum_piSingle]

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