spanSingleton_mul_coeIdeal_eq_coeIdeal

English

A similar equivalence when replacing z by IsLocalization.sec components in the localization.

Русский

Аналогичная эквивалентность при замене z на компоненты IsLocalization.sec.

LaTeX

$$spanSingleton R₁⁰ z * (I : FractionalIdeal R₁⁰ K) = J ↔ Ideal.span {((IsLocalization.sec R₁⁰ z).1 : R₁)} * I = Ideal.span {((IsLocalization.sec R₁⁰ z).2 : R₁)} * J$$

Lean4

theorem spanSingleton_mul_coeIdeal_eq_coeIdeal {I J : Ideal R₁} {z : K} :
    spanSingleton R₁⁰ z * (I : FractionalIdeal R₁⁰ K) = J ↔
      Ideal.span {((IsLocalization.sec R₁⁰ z).1 : R₁)} * I = Ideal.span {((IsLocalization.sec R₁⁰ z).2 : R₁)} * J :=
  by rw [← mk'_mul_coeIdeal_eq_coeIdeal K (IsLocalization.sec R₁⁰ z).2.prop, IsLocalization.mk'_sec K z]

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