le_div_iff

Mathlib.Algebra.Algebra.Operations

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

English

A ≤ J/K holds iff for all x ∈ I and z ∈ K, xz ∈ J.

Русский

Справедливо I ≤ J/K тогда и только тогда, когда для всех x ∈ I и z ∈ K имеет xz ∈ J.

LaTeX

$$$I \\le J/K \\iff \\forall x \\in I, \\forall z \\in K, x z \\in J$$$

Lean4

theorem le_div_iff {I J K : Submodule R A} : I ≤ J / K ↔ ∀ x ∈ I, ∀ z ∈ K, x * z ∈ J :=
  Iff.refl _

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

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

Разделы

Аффилиация

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