Documentation

Mathlib.Algebra.GroupWithZero.Divisibility

Divisibility in groups with zero. #

Lemmas about divisibility in groups and monoids with zero.

theorem eq_zero_of_zero_dvd {α : Type u_1} [SemigroupWithZero α] {a : α} (h : 0 a) :
a = 0
@[simp]
theorem zero_dvd_iff {α : Type u_1} [SemigroupWithZero α] {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.

@[simp]
theorem dvd_zero {α : Type u_1} [SemigroupWithZero α] (a : α) :
a 0
theorem mul_dvd_mul_iff_left {α : Type u_1} [CancelMonoidWithZero α] {a : α} {b : α} {c : α} (ha : a 0) :
a * b a * c b c

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

theorem mul_dvd_mul_iff_right {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {b : α} {c : α} (hc : c 0) :
a * c b * c a b

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

def DvdNotUnit {α : Type u_1} [CommMonoidWithZero α] (a : α) (b : α) :

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

Equations
Instances For
    theorem dvdNotUnit_of_dvd_of_not_dvd {α : Type u_1} [CommMonoidWithZero α] {a : α} {b : α} (hd : a b) (hnd : ¬b a) :
    theorem isRelPrime_zero_left {α : Type u_1} [CommMonoidWithZero α] {x : α} :
    theorem IsRelPrime.ne_zero_or_ne_zero {α : Type u_1} [CommMonoidWithZero α] {x : α} {y : α} [Nontrivial α] (h : IsRelPrime x y) :
    x 0 y 0
    theorem isRelPrime_of_no_nonunits_factors {α : Type u_1} [MonoidWithZero α] {x : α} {y : α} (nonzero : ¬(x = 0 y = 0)) (H : ∀ (z : α), ¬IsUnit zz 0z x¬z y) :
    theorem dvd_and_not_dvd_iff {α : Type u_1} [CancelCommMonoidWithZero α] {x : α} {y : α} :
    x y ¬y x DvdNotUnit x y
    theorem ne_zero_of_dvd_ne_zero {α : Type u_1} [MonoidWithZero α] {p : α} {q : α} (h₁ : q 0) (h₂ : p q) :
    p 0
    theorem isPrimal_zero {α : Type u_1} [MonoidWithZero α] :
    theorem IsPrimal.mul {α : Type u_2} [CancelCommMonoidWithZero α] {m : α} {n : α} (hm : IsPrimal m) (hn : IsPrimal n) :
    IsPrimal (m * n)
    theorem dvd_antisymm {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {b : α} [Subsingleton αˣ] :
    a bb aa = b
    theorem dvd_antisymm' {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {b : α} [Subsingleton αˣ] :
    a bb ab = a
    theorem Dvd.dvd.antisymm {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {b : α} [Subsingleton αˣ] :
    a bb aa = b

    Alias of dvd_antisymm.

    theorem Dvd.dvd.antisymm' {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {b : α} [Subsingleton αˣ] :
    a bb ab = a

    Alias of dvd_antisymm'.

    theorem eq_of_forall_dvd {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {b : α} [Subsingleton αˣ] (h : ∀ (c : α), a c b c) :
    a = b
    theorem eq_of_forall_dvd' {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {b : α} [Subsingleton αˣ] (h : ∀ (c : α), c a c b) :
    a = b
    theorem pow_dvd_pow_iff {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {m : } {n : } (ha₀ : a 0) (ha : ¬IsUnit a) :
    a ^ n a ^ m n m