matrix_map — Mathlib

English

If f is an embedding, then the entrywise map on matrices is an embedding.

Русский

Если f — вложение, то отображение матриц по элементам также является вложением.

LaTeX

$$$\\operatorname{IsEmbedding}(f) \\Rightarrow \\operatorname{IsEmbedding}\\bigl(\\operatorname{map}\\,\\cdot\\, f : \\text{Matrix}_{m\\times n}(R) \\to \\text{Matrix}_{m\\times n}(S)\\bigr)$$$

Lean4

theorem matrix_map (hf : IsEmbedding f) : IsEmbedding (map · f : Matrix m n R → Matrix m n S) :=
  IsEmbedding.piMap fun _ : m ↦ (IsEmbedding.piMap fun _ : n ↦ hf)

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