le_self_mul_one_div

Mathlib.Algebra.Algebra.Operations

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

English

If I is a submodule with I ≤ 1, then I ≤ I · (1/I).

Русский

Если I ⊆ 1, тогда I ⊆ I·(1/I).

LaTeX

$$I ≤ 1 → I ≤ I \cdot (1 / I)$$

Lean4

theorem le_self_mul_one_div {I : Submodule R A} (hI : I ≤ 1) : I ≤ I * (1 / I) := by
  simpa using mul_le_mul_left' (one_le_one_div.mpr hI) _

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

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

Разделы

Аффилиация

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