English
An element lies in the product spanSingleton x * I iff it can be written as x times some element of I.
Русский
Элемент принадлежит произведению spanSingleton x * I тогда, когда его можно записать как x на некоторый элемент I.
LaTeX
$$$y \\in spanSingleton S x * I \\iff \\exists y'\\in I,\\ y = x y'$$$
Lean4
theorem mem_singleton_mul {x y : P} {I : FractionalIdeal S P} : y ∈ spanSingleton S x * I ↔ ∃ y' ∈ I, y = x * y' :=
by
constructor
· intro h
refine FractionalIdeal.mul_induction_on h ?_ ?_
· intro x' hx' y' hy'
obtain ⟨a, ha⟩ := (mem_spanSingleton S).mp hx'
use a • y', Submodule.smul_mem (I : Submodule R P) a hy'
rw [← ha, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]
· rintro _ _ ⟨y, hy, rfl⟩ ⟨y', hy', rfl⟩
exact ⟨y + y', Submodule.add_mem (I : Submodule R P) hy hy', (mul_add _ _ _).symm⟩
· rintro ⟨y', hy', rfl⟩
exact mul_mem_mul ((mem_spanSingleton S).mpr ⟨1, one_smul _ _⟩) hy'
