Theorems · Theorem · group theory
Dvd.intro
∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ b- Defined in
- Mathlib.Algebra.Divisibility.Basic
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- Semigroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semigroupstatement and proof · cited by 202
Cited by26
Results whose statement or proof uses this declaration.
- dvd_reflproof · cited by 97
- dvd_mul_rightproof · cited by 89
- dvd_zeroproof · cited by 63
- dvd_mul_leftproof · cited by 47
- one_dvdproof · cited by 37
- dvd_addproof · cited by 25
- Dvd.intro_leftproof · cited by 20
- dvd_of_mul_right_eqproof · cited by 12
- dvd_of_mul_left_dvdproof · cited by 8
- Units.mul_right_dvdproof · cited by 7
- PNat.factorMultiset_le_iffproof · cited by 5
- Commute.sub_dvd_pow_sub_powproof · cited by 4