English
Two spans are equal if and only if there exists a unit z ∈ Rˣ with z · x = y.
Русский
Две области порождения совпадают тогда и только тогда существует единица z ∈ Rˣ с z · x = y.
LaTeX
$$$ \operatorname{spanSingleton} S x = \operatorname{spanSingleton} S y \iff \exists z \in R^{\times}, z \cdot x = y $$$
Lean4
/-- A version of `FractionalIdeal.den_mul_self_eq_num` in terms of fractional ideals. -/
theorem den_mul_self_eq_num' (I : FractionalIdeal S P) : spanSingleton S (algebraMap R P I.den) * I = I.num :=
by
apply coeToSubmodule_injective
dsimp only
rw [coe_mul, ← smul_eq_mul, coe_spanSingleton, smul_eq_mul, Submodule.span_singleton_mul]
convert I.den_mul_self_eq_num using 1
ext
rw [mem_smul_pointwise_iff_exists, mem_smul_pointwise_iff_exists]
simp [smul_eq_mul, Algebra.smul_def, Submonoid.smul_def]
