h_def — Mathlib

English

Equality characterization of h: h i equals a diagonal block form with a specified diagonal block.

Русский

Эквивалентное описание h: h i совпадает с блочной диагональной формой, где диагональный блок задан.

LaTeX

$$h i = .fromBlocks 0 0 0 (.diagonal (P.pairingIn ℤ · i))$$

Lean4

theorem h_def [DecidableEq ι] (i : b.support) : h i = .fromBlocks 0 0 0 (.diagonal (P.pairingIn ℤ · i)) := by
  ext (j | j) (k | k) <;> simp [h, Matrix.diagonal_apply]

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