le_traceDual

Mathlib.RingTheory.DedekindDomain.Different

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

English

Let I,J be submodules of L over B. Then I ≤ Jᵛ holds if and only if the product IJ lies in the dual of 1, i.e., IJ ≤ 1ᵛ.

Русский

Пусть I, J — подмодули L над B. Тогда I ⊆ Jᵛ эквивалентно тому, что IJ ≤ 1ᵛ.

LaTeX

$$$I \le J^\vee \iff I \cdot J \le 1^\vee.$$$

Lean4

theorem le_traceDual {I J : Submodule B L} : I ≤ Jᵛ ↔ I * J ≤ 1ᵛ := by rw [← le_traceDual_mul_iff, mul_one]

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

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

Разделы

Аффилиация

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