Theorems · Definition · group theory
RightDvd
{α : Type u_1} → [Semigroup α] → α → α → PropRight divisibility relation. RightDvd a b means a right-divides b,
i.e., ∃ c, b = c * a.
- Defined in
- Mathlib.Algebra.Divisibility.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 4 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 by13
Results whose statement or proof uses this declaration.
- RightDvd.mul_conststatement and proof · cited by 2
- RightDvd.mul_selfstatement · cited by 2
- RightDvd.transstatement and proof · cited by 2
- RightDvd.reflstatement · cited by 2
- RightDvd.of_eqstatement and proof · cited by 1
- RightDvd.mul_leftstatement and proof · cited by 0
- rightDvd_iff_dvdstatement · cited by 0
- rightDvd_iff_op_dvd_opstatement and proof · cited by 0
- Eq.rightDvdstatement · cited by 0
- RightDvd.of_mul_leftstatement and proof · cited by 0
- mul_rightDvd_mul_iff_leftstatement and proof · cited by 0
- RightDvd.rflstatement · cited by 0