mul_inv_eq_one

Mathlib.RingTheory.DedekindDomain.Ideal.Basic

URI: https://scilib.ai/kg/mathlib#IsDedekindDomainInv.mul_inv_eq_one

English

For any nonzero fractional ideal I in a Dedekind-inv domain, I · I^{-1} = 1.

Русский

Для любого не нулевого дробного идеала I в домене Дедекина выполняется I · I^{-1} = 1.

LaTeX

$$$$I \\neq 0 \\implies I \\cdot I^{-1} = 1.$$$$

Lean4

theorem mul_inv_eq_one {I : FractionalIdeal A⁰ K} (hI : I ≠ 0) : I * I⁻¹ = 1 :=
  isDedekindDomainInv_iff.mp h I hI

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

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

Разделы

Аффилиация

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