Congruence modulo multiples of an element in a (semi)field

In this file we prove a few theorems about the congruence relation _ ≡ _ [PMOD _] in a division semiring or a semifield.

@[simp]

theorem AddCommGroup.div_modEq_div {K : Type u_1} [DivisionSemiring K] {a b c p : K} (hc : c ≠ 0) : a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD p * c]

@[simp]

theorem AddCommGroup.mul_modEq_mul_right {K : Type u_1} [DivisionSemiring K] {a b c p : K} (hc : c ≠ 0) : a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p / c]

@[simp]

theorem AddCommGroup.mul_modEq_mul_left {K : Type u_1} [Semifield K] {a b c p : K} (hc : c ≠ 0) : c * a ≡ c * b [PMOD p] ↔ a ≡ b [PMOD p / c]