nsmul_mem_zmultiples_iff_exists_sub_div

English

In a Division Ring of CharZero, n ≠ 0 implies that n · r ∈ zmultiples(p) iff there exists k ∈ Fin n such that r − k(p/n) ∈ zmultiples(p).

Русский

В дивизионном кольце CharZero, для n ≠ 0 верно: n·r ∈ zmultiples(p) эквивалентно существованию k ∈ Fin n, такого что r − k(p/n) ∈ zmultiples(p).

LaTeX

$$$ n \neq 0 \Rightarrow n\cdot r \in \operatorname{zmultiples}(p) \iff \exists k: Fin(n),\ r - k\,(p/n) \in \operatorname{zmultiples}(p) $$$

Lean4

theorem nsmul_mem_zmultiples_iff_exists_sub_div {r : R} {n : ℕ} (hn : n ≠ 0) :
    n • r ∈ AddSubgroup.zmultiples p ↔ ∃ k : Fin n, r - (k : ℕ) • (p / n : R) ∈ AddSubgroup.zmultiples p :=
  by
  rw [← natCast_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.natCast_ne_zero.mpr hn), Int.cast_natCast]
  rfl

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