le_self_mul_self

Mathlib.RingTheory.FractionalIdeal.Basic

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

English

If I ≥ 1, then I ≤ I^2.

Русский

Если I ≥ 1, то I ≤ I^2.

LaTeX

$$$1 \le I \Rightarrow I \le I^2$$$

Lean4

theorem le_self_mul_self {I : FractionalIdeal S P} (hI : 1 ≤ I) : I ≤ I * I :=
  by
  convert mul_left_mono I hI
  exact (mul_one I).symm

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

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

Разделы

Аффилиация

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