matrix_monotone — Mathlib

English

The map I ↦ I.matrix n is monotone with respect to inclusion of two-sided ideals: if I ⊆ J then I.matrix n ⊆ J.matrix n.

Русский

Отображение I ↦ I.matrix n монотонно по включению: если I ⊆ J, то I.matrix n ⊆ J.matrix n.

LaTeX

$$$$ I \\subseteq J \\Rightarrow I^{\\mathrm{matrix}}_n \\subseteq J^{\\mathrm{matrix}}_n. $$$$

Lean4

theorem matrix_monotone : Monotone (matrix (R := R) n) := fun _ _ IJ _ MI i j => IJ (MI i j)

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