English
For fixed i, j, the function ofMatrix applied to c is equal to the map that sends (x, y) to c evaluated at the pair of rank-one matrices with a single (i, j)-entry x and y respectively.
Русский
Для фиксированных i, j функция ofMatrix, применяемая к c, равна отображению, отправляющему (x, y) в c( single i j x)(single i j y).
LaTeX
$$$$ \\forall x,y:\\; \\mathrm{ofMatrix}(c)(x,y) = c\\bigl(\\mathrm{single}_{i j} x\\bigr)\\bigl(\\mathrm{single}_{i j} y\\bigr). $$$$
Lean4
theorem coe_ofMatrix_eq_relationMap [DecidableEq n] {c : RingCon (Matrix n n R)} (i j : n) :
⇑(ofMatrix c) = Relation.Map c (· i j) (· i j) := by
ext x y
constructor
· intro h
refine ⟨_, _, h i j, ?_⟩
simp
· rintro ⟨X, Y, h, rfl, rfl⟩ i' j'
simpa using c.mul (c.mul (c.refl <| single i' i 1) h) (c.refl <| single j j' 1)
