mul_one_div_le_one

Mathlib.Algebra.Algebra.Operations

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

← MathLib Explorer

English

For any submodule I, the product I·(1/I) is contained in 1.

Русский

Для любого подмодуля I произведение I·(1/I) содержится в 1.

LaTeX

$$I \cdot (1 / I) \le 1$$

Lean4

theorem mul_one_div_le_one {I : Submodule R A} : I * (1 / I) ≤ 1 :=
  by
  rw [Submodule.mul_le]
  intro m hm n hn
  rw [Submodule.mem_div_iff_forall_mul_mem] at hn
  rw [mul_comm]
  exact hn m hm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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