English
For fixed i, j in n and for x, y in R, the relation given by ofMatrix c on x and y at the matrix level is equivalent to applying c to the matrices with a single nonzero entry at position (i, j): ofMatrix c x y ↔ c (single i j x) (single i j y).
Русский
Для фиксированных i, j ∈ n и элементов x, y ∈ R выполняется: ofMatrix c x y ↔ c (single i j x) (single i j y).
LaTeX
$$$$ \\mathrm{ofMatrix}(c\\, ,x, y) \\;\\Longleftrightarrow\\; c\\bigl(\\mathrm{single}_{i j} x\\bigr)\\bigl(\\mathrm{single}_{i j} y\\bigr). $$$$
Lean4
/-- A version of `ofMatrix_rel` for a single matrix index, rather than all indices. -/
theorem ofMatrix_rel' [DecidableEq n] {c : RingCon (Matrix n n R)} {x y : R} (i j : n) :
ofMatrix c x y ↔ c (single i j x) (single i j y) :=
by
refine ⟨fun h ↦ h i j, fun h i' j' ↦ ?_⟩
simpa using c.mul (c.mul (c.refl <| single i' i 1) h) (c.refl <| single j j' 1)
