matrix_bot

Mathlib.LinearAlgebra.Matrix.Ideal

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.matrix_bot

English

The matrix construction sends the bottom ideal to the bottom ideal: matrix n of ⊥ is ⊥.

Русский

Операция матричного идеала переводит нулевой идеал в нулевой: matrix n ⊥ = ⊥.

LaTeX

$$$$ \\mathrm{matrix}_n(\\perp) = \\perp. $$$$

Lean4

@[simp]
theorem matrix_bot : (⊥ : TwoSidedIdeal R).matrix n = ⊥ :=
  ringCon_injective <| RingCon.matrix_bot _

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

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

Разделы

Аффилиация

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