Mathlib Map

Theorems · Theorem · group theory

pow_dvd_pow

∀ {α : Type u_1} [inst : Monoid α] {m n : ℕ} (a : α), m ≤ n → a ^ m ∣ a ^ n
Defined in
Mathlib.Algebra.Divisibility.Basic
Cited by
56 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Nat.factorization_le_iff_dvd · cited by 18Nat.factorization_le_iff_…Polynomial.le_rootMultiplicity_iff · cited by 10Polynomial.le_rootMultipl…PadicInt.limNthHom · cited by 8PadicInt.limNthHomdvd_prime_pow · cited by 6dvd_prime_powPadicInt.lift · cited by 6PadicInt.liftemultiplicity_eq_of_dvd_of_not_dvd · cited by 5emultiplicity_eq_of_dvd_o…PadicInt.nthHomSeq · cited by 4PadicInt.nthHomSeqPadicInt.zmod_cast_comp_toZModPow · cited by 4PadicInt.zmod_cast_comp_t…Nat.dvd_prod_primeFactors_pow_self · cited by 4Nat.dvd_prod_primeFactors…IsPrimitiveRoot.norm_pow_sub_one_two · cited by 3IsPrimitiveRoot.norm_pow_…pow_dvd_pow_of_dvd_of_le · cited by 3pow_dvd_pow_of_dvd_of_lePadicInt.isCauSeq_nthHom · cited by 3PadicInt.isCauSeq_nthHomnot_pow_dvd_of_emultiplicity_lt · cited by 3not_pow_dvd_of_emultiplic…PadicInt.lift_spec · cited by 3PadicInt.lift_specPadicInt.pow_dvd_nthHom_sub · cited by 2PadicInt.pow_dvd_nthHom_s…Monoid · cited by 3887Monoidpow_add · cited by 315pow_addpow_dvd_powCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Monoidstatement and proof · cited by 3,887
  • pow_addproof · cited by 315

Cited by59

Results whose statement or proof uses this declaration.