dvd_bot

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.dvd_bot

English

If I divides J (in the ideal sense), then J ≤ I.

Русский

Если I делит J в смысле идеалов, то J ≤ I.

LaTeX

$$$ I \mid J \Rightarrow J \le I $$$

Lean4

@[simp]
theorem dvd_bot {I : Ideal R} : I ∣ ⊥ :=
  dvd_zero I

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

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

Разделы

Аффилиация

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