mem_matrix

Mathlib.LinearAlgebra.Matrix.Ideal

URI: https://scilib.ai/kg/mathlib#Ideal.mem_matrix

English

An element M of a matrix ring lies in I.matrix if and only if each entry M_{ij} lies in I.

Русский

Элемент M кольца матриц принадлежит I.matrix тогда и лишь тогда, когда каждый элемент M_{ij} принадлежит I.

LaTeX

$$M ∈ I.matrix n ↔ ∀ i j, M_{ij} ∈ I$$

Lean4

@[simp]
theorem mem_matrix (I : Ideal R) (M : Matrix n n R) : M ∈ I.matrix n ↔ ∀ i j, M i j ∈ I := by rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru