dual_involutive

Mathlib.RingTheory.DedekindDomain.Different

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

English

Applying the dual operator twice yields the original ideal: dual(dual(I)) = I.

Русский

После применения двойственной операции дважды получаем исходный идеал: dual(dual(I)) = I.

LaTeX

$$\mathrm{dual}_{A,K}(\mathrm{dual}_{A,K}(I)) = I$$

Lean4

theorem dual_involutive : Function.Involutive (dual A K : FractionalIdeal B⁰ L → FractionalIdeal B⁰ L) :=
  dual_dual A K

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

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

Разделы

Аффилиация

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