coe_dual

Mathlib.RingTheory.DedekindDomain.Different

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.coe_dual

English

The dual of the unit fractional ideal is the unit trace-dual: 1ᵛ.

Русский

Дуальность единичного дробного идеала дает единичную дуальность по следу: 1ᶟ.

LaTeX

$$dual A K (1 : FractionalIdeal B⁰ L) = 1ᵛ.$$

Lean4

theorem coe_dual (hI : I ≠ 0) : (dual A K I : Submodule B L) = Iᵛ := by rw [dual, dif_neg hI, coe_mk]

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

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

Разделы

Аффилиация

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