Lemmas about quotients in characteristic zero #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem add_subgroup.zsmul_mem_zmultiples_iff_exists_sub_div {R : Type u_1} [division_ring R] [char_zero R] {p r : R} {z : ℤ} (hz : z ≠ 0) :

z • r is a multiple of p iff r is pk/z above a multiple of p, where 0 ≤ k < |z|.

theorem add_subgroup.nsmul_mem_zmultiples_iff_exists_sub_div {R : Type u_1} [division_ring R] [char_zero R] {p r : R} {n : ℕ} (hn : n ≠ 0) :

theorem quotient_add_group.zmultiples_zsmul_eq_zsmul_iff {R : Type u_1} [division_ring R] [char_zero R] {p : R} {ψ θ : R ⧸ add_subgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) :

z • ψ = z • θ ↔ ∃ (k : fin z.nat_abs), ψ = θ + ↑k • ↑(p / ↑z)

theorem quotient_add_group.zmultiples_nsmul_eq_nsmul_iff {R : Type u_1} [division_ring R] [char_zero R] {p : R} {ψ θ : R ⧸ add_subgroup.zmultiples p} {n : ℕ} (hz : n ≠ 0) :

n • ψ = n • θ ↔ ∃ (k : fin n), ψ = θ + ↑k • ↑(p / ↑n)