kroneckerMap_one_one — Mathlib

English

If the units are identity matrices and f(0,b)=0, f(a,0)=0, and f(1,1)=1, then kroneckerMap f (1) (1) = 1.

Русский

Если единичные матрицы заданы условиями f(0,b)=0, f(a,0)=0 и f(1,1)=1, то kroneckerMap f (1) (1) = 1.

LaTeX

$$$\operatorname{kroneckerMap} f (I_m) (I_n) = I_{mn}$ при $f(1,1)=1$ и соответствующих нулях.$$

Lean4

@[simp]
theorem kroneckerMap_one_one [Zero α] [Zero β] [Zero γ] [One α] [One β] [One γ] [DecidableEq m] [DecidableEq n]
    (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0) (hf₃ : f 1 1 = 1) :
    kroneckerMap f (1 : Matrix m m α) (1 : Matrix n n β) = 1 :=
  (kroneckerMap_diagonal_diagonal _ hf₁ hf₂ _ _).trans <| by simp only [hf₃, diagonal_one]

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