English
For ψ, θ in a quotient by zmultiples(p) and z ∈ ℤ, z ≠ 0, z · ψ = z · θ iff there exists k in Fin z.natAbs such that ψ = θ + k·(p/z).
Русский
Для ψ, θ в фактор-море по zmultiples(p) и z ∈ ℤ, z ≠ 0, выполняется z·ψ = z·θ тогда и только тогда, когда существует k ∈ Fin(|z|) такое, что ψ = θ + k·(p/z).
LaTeX
$$$ \forall \psi,\theta \in R / \operatorname{zmultiples}(p),\ z \in \mathbb{Z},\ z \neq 0:\ z\cdot \psi = z\cdot \theta \iff \exists k \in Fin(z.natAbs),\ \psi = \theta + k \cdot (p/z) $$$
Lean4
theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) :
z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + ((k : ℕ) • (p / z) : R) :=
by
induction ψ using Quotient.inductionOn
induction θ using Quotient.inductionOn
simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add, QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ←
sub_sub]
exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz
