mathlib3 documentation

algebra.group_with_zero.divisibility

Divisibility in groups with zero. #

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

Lemmas about divisibility in groups and monoids with zero.

source
theorem eq_zero_of_zero_dvd {α : Type u_1} [semigroup_with_zero α] {a : α} (h : 0 ∣ a) :
a = 0
source
@[simp]
theorem zero_dvd_iff {α : Type u_1} [semigroup_with_zero α] {a : α} :
0 ∣ a ↔ a = 0

Given an element a of a commutative semigroup with zero, there exists another element whose product with zero equals a iff a equals zero.

source
@[simp]
theorem dvd_zero {α : Type u_1} [semigroup_with_zero α] (a : α) :
a ∣ 0
source
theorem mul_dvd_mul_iff_left {α : Type u_1} [cancel_monoid_with_zero α] {a b c : α} (ha : a ≠ 0) :
a * b ∣ a * c ↔ b ∣ c

Given two elements b, c of a cancel_monoid_with_zero and a nonzero element a, a*b divides a*c iff b divides c.

source
theorem mul_dvd_mul_iff_right {α : Type u_1} [cancel_comm_monoid_with_zero α] {a b c : α} (hc : c ≠ 0) :
a * c ∣ b * c ↔ a ∣ b

Given two elements a, b of a commutative cancel_monoid_with_zero and a nonzero element c, a*c divides b*c iff a divides b.

source
def dvd_not_unit {α : Type u_1} [comm_monoid_with_zero α] (a b : α) :
Prop

dvd_not_unit a b expresses that a divides b "strictly", i.e. that b divided by a is not a unit.

Equations
source
theorem dvd_not_unit_of_dvd_of_not_dvd {α : Type u_1} [comm_monoid_with_zero α] {a b : α} (hd : a ∣ b) (hnd : ¬b ∣ a) :
dvd_not_unit a b
source
theorem dvd_and_not_dvd_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] {x y : α} :
x ∣ y ∧ ¬y ∣ x ↔ dvd_not_unit x y
source
theorem ne_zero_of_dvd_ne_zero {α : Type u_1} [monoid_with_zero α] {p q : α} (h₁ : q ≠ 0) (h₂ : p ∣ q) :
p ≠ 0
source
theorem dvd_antisymm {α : Type u_1} [cancel_comm_monoid_with_zero α] [subsingleton αˣ] {a b : α} :
a ∣ b → b ∣ a → a = b
source
theorem dvd_antisymm' {α : Type u_1} [cancel_comm_monoid_with_zero α] [subsingleton αˣ] {a b : α} :
a ∣ b → b ∣ a → b = a
source
theorem has_dvd.dvd.antisymm {α : Type u_1} [cancel_comm_monoid_with_zero α] [subsingleton αˣ] {a b : α} :
a ∣ b → b ∣ a → a = b

Alias of dvd_antisymm.

source
theorem has_dvd.dvd.antisymm' {α : Type u_1} [cancel_comm_monoid_with_zero α] [subsingleton αˣ] {a b : α} :
a ∣ b → b ∣ a → b = a

Alias of dvd_antisymm'.

source
theorem eq_of_forall_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [subsingleton αˣ] {a b : α} (h : ∀ (c : α), a ∣ c ↔ b ∣ c) :
a = b
source
theorem eq_of_forall_dvd' {α : Type u_1} [cancel_comm_monoid_with_zero α] [subsingleton αˣ] {a b : α} (h : ∀ (c : α), c ∣ a ↔ c ∣ b) :
a = b