mem_of_dvd

Mathlib.RingTheory.Ideal.Defs

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

English

If a divides b and a ∈ I, then b ∈ I.

Русский

Если a делит b и a ∈ I, то b ∈ I.

LaTeX

$$$\forall I\; (I: \text{Ideal } \alpha) \; \forall a,b \in \alpha, \; (a \mid b) \rightarrow (a \in I) \rightarrow (b \in I).$$$

Lean4

theorem mem_of_dvd (hab : a ∣ b) (ha : a ∈ I) : b ∈ I := by obtain ⟨c, rfl⟩ := hab; exact I.mul_mem_right _ ha

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

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

Разделы

Аффилиация

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