constant_factor_ne_zero — Mathlib

English

If an I is nonzero and I = a⁻¹ J, then J is nonzero.

Русский

Если дробный идеал I ненулевой и I = a⁻¹ J, то J ненулевой.

LaTeX

$$If I ≠ 0 and I = spanSingleton R⁰ (algebraMap R K a)⁻¹ * ↑J, then J ≠ 0$$

Lean4

/-- If `I` is a nonzero fractional ideal, `a ∈ R`, and `J` is an ideal of `R` such that
`I = a⁻¹J`, then `a` is nonzero. -/
theorem constant_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) : (Ideal.span { a } : Ideal R) ≠ 0 := fun h ↦
  by
  rw [Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] at h
  rw [h, RingHom.map_zero, inv_zero, spanSingleton_zero, zero_mul] at haJ
  exact hI haJ

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