toSubring_mono

Mathlib.RingTheory.LocalRing.LocalSubring

URI: https://scilib.ai/kg/mathlib#LocalSubring.toSubring_mono

English

toSubring is monotone: if X ≤ Y then toSubring X ≤ toSubring Y.

Русский

toSubring монотонна: если X ≤ Y, тогда toSubring X ≤ toSubring Y.

LaTeX

$$Monotone LocalSubring.toSubring$$

Lean4

theorem toSubring_mono : Monotone (toSubring (R := R)) := fun _ _ e ↦ e.1

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

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

Разделы

Аффилиация

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