English
If I and J are fractional ideals, then their product I · J is again a fractional ideal.
Русский
Если I и J — дробные идеалы, то их произведение I · J снова дробный идеал.
LaTeX
$$IsFractional S I \to IsFractional S J \to IsFractional S (I * J)$$
Lean4
theorem _root_.IsFractional.mul {I J : Submodule R P} :
IsFractional S I → IsFractional S J → IsFractional S (I * J : Submodule R P)
| ⟨aI, haI, hI⟩, ⟨aJ, haJ, hJ⟩ =>
⟨aI * aJ, S.mul_mem haI haJ, fun b hb =>
by
refine Submodule.mul_induction_on hb ?_ ?_
· intro m hm n hn
obtain ⟨n', hn'⟩ := hJ n hn
rw [mul_smul, mul_comm m, ← smul_mul_assoc, ← hn', ← Algebra.smul_def]
apply hI
exact Submodule.smul_mem _ _ hm
· intro x y hx hy
rw [smul_add]
apply isInteger_add hx hy⟩
