invertible_of_principal — Mathlib

English

If I is principal and nonzero, then I is invertible, i.e., I I^{-1} = 1.

Русский

Если I является порожденным и не нулевой, то I обратимо, т.е. I I^{-1} = 1.

LaTeX

$$$$\text{If } I \text{ is principal and } I \neq 0,\; I \cdot I^{-1} = 1.$$$

Lean4

theorem invertible_of_principal (I : FractionalIdeal R₁⁰ K) [Submodule.IsPrincipal (I : Submodule R₁ K)] (h : I ≠ 0) :
    I * I⁻¹ = 1 :=
  mul_div_self_cancel_iff.mpr ⟨spanSingleton _ (generator (I : Submodule R₁ K))⁻¹, mul_generator_self_inv _ I h⟩

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