dual_inv

Mathlib.RingTheory.DedekindDomain.Different

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

English

The dual of the inverse of I equals the dual of 1 multiplied by I: dual(I^{-1}) = dual(1) · I.

Русский

Двойственная к I^{-1} равна двойственной к 1, умноженной на I: dual(I^{-1}) = dual(1) · I.

LaTeX

$$\mathrm{dual}_{A,K}(I^{-1}) = \mathrm{dual}_{A,K}(1) \cdot I$$

Lean4

theorem dual_inv : dual A K I⁻¹ = dual A K 1 * I := by rw [dual_eq_mul_inv, inv_inv]

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

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

Разделы

Аффилиация

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