English
Given a ring-con c and indices i, j and scalars x, y, the matrix c.matrix n (single i j x) (single i j y) encodes c x y entrywise and is equivalent to c x y for appropriate indices.
Русский
Пусть дан RingCon c и индексы i, j и скаляры x, y. Матрица c.matrix n (single i j x) (single i j y) кодирует отношение c на элементы и эквивалентна c x y при корректных индексах.
LaTeX
$$c.matrix n (Matrix.single i j x) (Matrix.single i j y) ↔ c x y$$
Lean4
@[simp]
theorem matrix_apply_single [DecidableEq n] {c : RingCon R} {i j : n} {x y : R} :
c.matrix n (Matrix.single i j x) (Matrix.single i j y) ↔ c x y :=
by
refine ⟨fun h ↦ by simpa using h i j, fun h i' j' ↦ ?_⟩
obtain hi | rfl := ne_or_eq i i'
· simpa [hi] using c.refl 0
obtain hj | rfl := ne_or_eq j j'
· simpa [hj] using c.refl _
simpa using h
