Mathlib Map

Theorems · Theorem · group theory

pow_dvd_pow_iff

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a : α} {m n : ℕ},
  a ≠ 0 → ¬IsUnit a → (a ^ n ∣ a ^ m ↔ n ≤ m)
Defined in
Mathlib.Algebra.GroupWithZero.Divisibility
Cited by
1 results in Mathlib
Foundations
Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommMonoidWithZeroIsCancelMulZero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

emultiplicity_pow_self · cited by 3emultiplicity_pow_selfmul_one · cited by 3885mul_oneIsUnit · cited by 1602IsUnitCommMonoidWithZero · cited by 913CommMonoidWithZeropow_succ · cited by 374pow_succnot_lt · cited by 306not_ltpow_ne_zero · cited by 208pow_ne_zeroIsCancelMulZero · cited by 177IsCancelMulZeroDvd.dvd.trans · cited by 148dvd.transpow_dvd_pow · cited by 56pow_dvd_powmul_dvd_mul_iff_left · cited by 24mul_dvd_mul_iff_leftisUnit_iff_dvd_one · cited by 21isUnit_iff_dvd_onepow_dvd_pow_iffCITED BYCITES

Cites11

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

Cited by1

Results whose statement or proof uses this declaration.