one_le_one_div

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.one_le_one_div

English

Let I be a submodule. Then 1 ≤ 1/I if and only if I ≤ 1.

Русский

Пусть I — подмодуль. Тогда 1 ≤ 1/I тогда и только тогда I ≤ 1.

LaTeX

$$$1 \le 1 / I \iff I \le 1$$$

Lean4

theorem one_le_one_div {I : Submodule R A} : 1 ≤ 1 / I ↔ I ≤ 1 := by rw [le_div_iff_mul_le, one_mul]

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

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

Разделы

Аффилиация

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