one_mem_div

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.one_mem_div

English

For submodules I, J of A, 1 belongs to I/J if and only if J is contained in I.

Русский

Для подмодулей I, J ⊆ A выполняется: 1 принадлежит I/J тогда и только тогда J ⊆ I.

LaTeX

$$"1 ∈ I / J" ↔ "J ≤ I"$$

Lean4

@[simp]
theorem one_mem_div {I J : Submodule R A} : 1 ∈ I / J ↔ J ≤ I := by rw [← one_le, le_div_iff_mul_le, one_mul]

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

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

Разделы

Аффилиация

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