Theorems · Theorem · group theory
Dvd.intro_left
∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ b- Defined in
- Mathlib.Algebra.Divisibility.Basic
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- CommSemigroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_commproof · cited by 2,262
- CommSemigroupstatement and proof · cited by 62
- Dvd.introproof · cited by 26
Cited by20
Results whose statement or proof uses this declaration.
- dvd_of_mul_left_eqproof · cited by 14
- Nat.snd_mem_divisors_of_mem_antidiagonalproof · cited by 4
- Subgroup.card_dvd_of_surjectiveproof · cited by 3
- AddSubgroup.card_dvd_of_surjectiveproof · cited by 3
- Polynomial.IsPrimitive.dvd_primPart_iff_dvdproof · cited by 2
- Polynomial.IsPrimitive.irreducible_of_irreducible_map_of_injectiveproof · cited by 2
- orderOf_eq_of_pow_and_pow_div_primeproof · cited by 2
- ZMod.isCyclic_units_of_prime_powproof · cited by 2
- irrational_nrt_of_notint_nrtproof · cited by 2
- Rat.den_div_intCast_eq_one_iffproof · cited by 2
- Ring.ord_le_ord_mulproof · cited by 1
- Polynomial.primPart_dvdproof · cited by 1