mem_dual

Mathlib.RingTheory.DedekindDomain.Different

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

← MathLib Explorer

English

The dual of the zero fractional ideal is zero: dual 0 = 0.

Русский

Дуальность нулевого дробного идеала равна нулю: dual 0 = 0.

LaTeX

$$dual_zero : dual A K (0 : FractionalIdeal B⁰ L) = 0.$$

Lean4

theorem mem_dual (hI : I ≠ 0) {x} : x ∈ dual A K I ↔ ∀ a ∈ I, traceForm K L x a ∈ (algebraMap A K).range := by
  rw [dual, dif_neg hI]; exact forall₂_congr fun _ _ ↦ mem_one

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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