Lemmas about divisibility in rings #
Note that this file is imported by basic tactics like linarith
and so must have only minimal
imports. Further results about divisibility in rings may be found in
Mathlib.Algebra.Ring.Divisibility.Lemmas
which is not subject to this import constraint.
theorem
MulEquiv.decompositionMonoid
{α : Type u_1}
{β : Type u_2}
[Semigroup α]
[Semigroup β]
{F : Type u_3}
[EquivLike F α β]
[MulEquivClass F α β]
(f : F)
[DecompositionMonoid β]
:
Alias of the reverse direction of neg_dvd
.
The negation of an element a
of a semigroup with a distributive negation divides another
element b
iff a
divides b
.
Alias of the forward direction of neg_dvd
.
The negation of an element a
of a semigroup with a distributive negation divides another
element b
iff a
divides b
.