isPrincipal_iff — Mathlib

English

A fractional ideal I is principal if and only if I.coeToSubmodule is principal, i.e., there exists x with I = spanSingleton S x.

Русский

Дробный идеал I является главным тогда и только тогда, когда I.coeToSubmodule главное, то есть существует x: I = spanSingleton S x.

LaTeX

$$$ \text{IsPrincipal}(I) \iff \exists x, I = \operatorname{spanSingleton} S x $$$

Lean4

theorem isPrincipal_iff (I : FractionalIdeal S P) : IsPrincipal (I : Submodule R P) ↔ ∃ x, I = spanSingleton S x :=
  ⟨fun _ => ⟨generator (I : Submodule R P), eq_spanSingleton_of_principal I⟩, fun ⟨x, hx⟩ =>
    { principal := ⟨x, Eq.trans (congr_arg _ hx) (coe_spanSingleton _ x)⟩ }⟩

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