le_self_mul_inv

Mathlib.RingTheory.FractionalIdeal.Inverse

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.le_self_mul_inv

English

If I ≤ 1, then I ≤ I I^{-1}.

Русский

Если I ≤ 1, то I ≤ I I^{-1}.

LaTeX

$$$$I \le 1 \Rightarrow I \le I \cdot I^{-1}.$$$$

Lean4

theorem le_self_mul_inv {I : FractionalIdeal R₁⁰ K} (hI : I ≤ (1 : FractionalIdeal R₁⁰ K)) : I ≤ I * I⁻¹ :=
  le_self_mul_one_div hI

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

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

Разделы

Аффилиация

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