eq_spanSingleton_of_principal — Mathlib

English

If I is a fractional ideal with isomorphic substructure, then I = spanSingleton S (generator of I.coeToSubmodule).

Русский

Если дробный идеал I имеет заданное подструктурное изоморфное представление, то I = spanSingleton S (генератор I.coeToSubmodule).

LaTeX

$$$ I = \operatorname{spanSingleton} S (\text{generator}(I_{\text{coeToSubmodule}})) $$$

Lean4

theorem eq_spanSingleton_of_principal (I : FractionalIdeal S P) [IsPrincipal (I : Submodule R P)] :
    I = spanSingleton S (generator (I : Submodule R P)) := by
  -- Porting note: this used to be `coeToSubmodule_injective (span_singleton_generator ↑I).symm`
    -- but Lean 4 struggled to unify everything. Turned it into an explicit `rw`.
  rw [spanSingleton, ← coeToSubmodule_inj, coe_mk, span_singleton_generator]

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