ideal_factor_ne_zero — Mathlib

English

A variant expression for representing I as spanSingleton of x inverse times a sub-ideal.

Русский

Вариант выражения для представления I как spanSingleton от x⁻¹ умноженного на подидеал.

LaTeX

$$∃ a ∈ R, ∃ aI, a ≠ 0 ∧ I = spanSingleton R⁰ (algebraMap R K a)⁻¹ * aI$$

Lean4

/-- If `I` is a nonzero fractional ideal, `a ∈ R`, and `J` is an ideal of `R` such that
`I = a⁻¹J`, then `J` is nonzero. -/
theorem ideal_factor_ne_zero {R} [CommRing R] {K : Type*} [Field K] [Algebra R K] [IsFractionRing R K]
    {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) {a : R} {J : Ideal R}
    (haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J) : J ≠ 0 := fun h ↦
  by
  rw [h, Ideal.zero_eq_bot, coeIdeal_bot, mul_zero] at haJ
  exact hI haJ

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