Zulip Chat Archive
Stream: Is there code for X?
Topic: dvd_of_pow_dvd_pow
Ruben Van de Velde (Sep 24 2020 at 07:30):
example (n m k : nat) (h : m ^ k ∣ n ^ k) (hpos : 0 < k) : (m ∣ k) := sorry
Ruben Van de Velde (Sep 24 2020 at 07:34):
Helps if I don't typo the m ∣ n - it's (nat.pow_dvd_pow_iff hpos).mp h
Last updated: May 02 2025 at 03:31 UTC