mul_inv_cancel_iff_isUnit

Mathlib.RingTheory.FractionalIdeal.Inverse

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

English

I ∗ I^{-1} = 1 if and only if I is a unit.

Русский

I ∗ I^{-1} = 1 тогда и только тогда, когда I является единицей в заднем кольце.

LaTeX

$$$$I \cdot I^{-1} = 1 \iff \text{IsUnit}(I).$$$$

Lean4

theorem mul_inv_cancel_iff_isUnit {I : FractionalIdeal R₁⁰ K} : I * I⁻¹ = 1 ↔ IsUnit I :=
  (mul_inv_cancel_iff K).trans isUnit_iff_exists_inv.symm

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

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

Разделы

Аффилиация

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