dual_mul_self

Mathlib.RingTheory.DedekindDomain.Different

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

English

If I ≠ 0, then the dual of I multiplied by I gives the dual of 1: dual(I) · I = dual(1).

Русский

Если I ≠ 0, то дуальная(I) умноженная на I даёт дуальную единицу: dual(I) · I = dual(1).

LaTeX

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

Lean4

theorem dual_mul_self (hI : I ≠ 0) : dual A K I * I = dual A K 1 := by
  rw [dual_eq_mul_inv, mul_assoc, inv_mul_cancel₀ hI, mul_one]

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

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

Разделы

Аффилиация

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