English
If I,J are fractional and J ≠ 0, then I / J is fractional.
Русский
Если I,J дробные и J ≠ 0, то I / J дробный.
LaTeX
$$IsFractional (nonZeroDivisors R₁) I → IsFractional (nonZeroDivisors R₁) J → Ne J 0 → IsFractional (nonZeroDivisors R₁) (instHDiv.hDiv I J)$$
Lean4
theorem _root_.IsFractional.div_of_nonzero {I J : Submodule R₁ K} :
IsFractional R₁⁰ I → IsFractional R₁⁰ J → J ≠ 0 → IsFractional R₁⁰ (I / J)
| ⟨aI, haI, hI⟩, ⟨aJ, haJ, hJ⟩, h =>
by
obtain ⟨y, mem_J, notMem_zero⟩ := SetLike.exists_of_lt (show 0 < J by simpa only using bot_lt_iff_ne_bot.mpr h)
obtain ⟨y', hy'⟩ := hJ y mem_J
use aI * y'
constructor
· apply (nonZeroDivisors R₁).mul_mem haI (mem_nonZeroDivisors_iff_ne_zero.mpr _)
intro y'_eq_zero
have : algebraMap R₁ K aJ * y = 0 := by rw [← Algebra.smul_def, ← hy', y'_eq_zero, RingHom.map_zero]
have y_zero :=
(mul_eq_zero.mp this).resolve_left
(mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).1 (IsFractionRing.injective _ _) _)
(mem_nonZeroDivisors_iff_ne_zero.mp haJ))
apply notMem_zero
simpa
intro b hb
convert hI _ (hb _ (Submodule.smul_mem _ aJ mem_J)) using 1
rw [← hy', mul_comm b, ← Algebra.smul_def, mul_smul]
