mul_self_le_self

Mathlib.RingTheory.FractionalIdeal.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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