Documentation

Mathlib.Algebra.CharZero.Quotient

Lemmas about quotients in characteristic zero #

theorem AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div {R : Type u_1} [DivisionRing R] [CharZero R] {p : R} {r : R} {z : } (hz : z 0) :
z r AddSubgroup.zmultiples p ∃ (k : Fin z.natAbs), r - k (p / z) AddSubgroup.zmultiples p

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

theorem AddSubgroup.nsmul_mem_zmultiples_iff_exists_sub_div {R : Type u_1} [DivisionRing R] [CharZero R] {p : R} {r : R} {n : } (hn : n 0) :
n r AddSubgroup.zmultiples p ∃ (k : Fin n), r - k (p / n) AddSubgroup.zmultiples p
theorem QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff {R : Type u_1} [DivisionRing R] [CharZero R] {p : R} {ψ : R AddSubgroup.zmultiples p} {θ : R AddSubgroup.zmultiples p} {z : } (hz : z 0) :
z ψ = z θ ∃ (k : Fin z.natAbs), ψ = θ + (k (p / z))
theorem QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff {R : Type u_1} [DivisionRing R] [CharZero R] {p : R} {ψ : R AddSubgroup.zmultiples p} {θ : R AddSubgroup.zmultiples p} {n : } (hz : n 0) :
n ψ = n θ ∃ (k : Fin n), ψ = θ + k (p / n)