diagonal_injective — Mathlib

English

The function mapping a diagonal descriptor to its matrix is injective.

Русский

Функция, отправляющая диагональное описание в диагональную матрицу, инъективна.

LaTeX

$$$\\text{Injective}\\ (\\mathrm{diagonal}) :\\; (d_1 = d_2) \\Rightarrow (\\mathrm{diagonal}\,d_1 = \\mathrm{diagonal}\,d_2)$$$

Lean4

theorem diagonal_injective [Zero α] : Function.Injective (diagonal : (n → α) → Matrix n n α) := fun d₁ d₂ h =>
  funext fun i => by simpa using Matrix.ext_iff.mpr h i i

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