zmultiples_nsmul_eq_nsmul_iff — Mathlib

English

For ψ, θ in a quotient by zmultiples(p) and n ∈ ℕ with n ≠ 0, n · ψ = n · θ iff there exists k ∈ Fin n with ψ = θ + k·(p/n).

Русский

Для ψ, θ в фактор-море по zmultiples(p) и n ∈ ℕ, n ≠ 0, выполняется n·ψ = n·θ ⇔ существует k ∈ Fin n такое, что ψ = θ + k·(p/n).

LaTeX

$$$ \forall \psi,\theta \in R / \operatorname{zmultiples}(p),\ n \in \mathbb{N},\ n \neq 0:\ n\cdot \psi = n\cdot \theta \iff \exists k : Fin\ n,\ \psi = \theta + k \cdot (p/n) $$$

Lean4

theorem zmultiples_nsmul_eq_nsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {n : ℕ} (hz : n ≠ 0) :
    n • ψ = n • θ ↔ ∃ k : Fin n, ψ = θ + (k : ℕ) • (p / n : R) :=
  by
  rw [← natCast_zsmul ψ, ← natCast_zsmul θ, zmultiples_zsmul_eq_zsmul_iff (Int.natCast_ne_zero.mpr hz),
    Int.cast_natCast]
  rfl

Похожие утверждения