matrix_apply — Mathlib

English

The action of RingCon.matrix is pointwise: applying the relation c to two matrices M and N is equivalent to requiring c to relate every corresponding entry M_{ij} and N_{ij}.

Русский

Действие RingCon.matrix сводится к покомпонентному отношению: применяя отношение c к двум матрицам M и N, эквивалентно требовать, чтобы c связывало каждую соответствующую пару элементов M_{ij} и N_{ij}.

LaTeX

$$c.matrix n M N ⇔ ∀ i j, c(M_{i j}, N_{i j})$$

Lean4

@[simp low]
theorem matrix_apply {c : RingCon R} {M N : Matrix n n R} : c.matrix n M N ↔ ∀ i j, c (M i j) (N i j) :=
  Iff.rfl

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