isPrincipal_inv — Mathlib

English

If I is a fractional ideal with principal underlying submodule and I ≠ 0, then its inverse I^{-1} is again principal.

Русский

Если I — дробный идеал с порождающим подмодулем и I ≠ 0, то его обратный I^{-1} снова порожден.

LaTeX

$$There exists a principal submodule structure for I^{-1}, i.e., I^{-1} is principal when I ≠ 0 and I is principal.$$

Lean4

theorem isPrincipal_inv (I : FractionalIdeal R₁⁰ K) [Submodule.IsPrincipal (I : Submodule R₁ K)] (h : I ≠ 0) :
    Submodule.IsPrincipal I⁻¹.1 := by
  rw [val_eq_coe, isPrincipal_iff]
  use (generator (I : Submodule R₁ K))⁻¹
  have hI : I * spanSingleton _ (generator (I : Submodule R₁ K))⁻¹ = 1 := mul_generator_self_inv _ I h
  exact (right_inverse_eq _ I (spanSingleton _ (generator (I : Submodule R₁ K))⁻¹) hI).symm

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