mul_inv_cancel_iff — Mathlib

English

For any fractional ideal I, I I^{-1} = 1 iff there exists J with I J = 1.

Русский

Для любого дробного идеала I, I I^{-1} = 1 тогда и только тогда, когда существует J с I J = 1.

LaTeX

$$$$I \cdot I^{-1} = 1 \;\text{ iff }\; \exists J,\; I \cdot J = 1.$$$$

Lean4

theorem mul_inv_cancel_iff {I : FractionalIdeal R₁⁰ K} : I * I⁻¹ = 1 ↔ ∃ J, I * J = 1 :=
  ⟨fun h => ⟨I⁻¹, h⟩, fun ⟨J, hJ⟩ => by rwa [← right_inverse_eq K I J hJ]⟩

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