mathlib documentation

algebra.char_zero.quotient

Lemmas about quotients in characteristic zero #

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

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)