instPosMulStrictMonoIdeal

Mathlib.RingTheory.DedekindDomain.Ideal.Basic

URI: https://scilib.ai/kg/mathlib#instPosMulStrictMonoIdeal

English

For ideals, fixed nonzero multiplication is strictly monotone: if I < J, then I · X < J · X for fixed X ≠ 0.

Русский

Для идеалов фиксированное ненулевое умножение строго монотонно: если I < J, то I·X < J·X для фиксированного X ≠ 0.

LaTeX

$$$\mathrm{PosMulStrictMono}(\mathrm{Ideal}(A))$$$

Lean4

instance : PosMulStrictMono (Ideal A) :=
  PosMulMono.toPosMulStrictMono

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

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

Разделы

Аффилиация

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