permu

Stream: new members

[vxctyxeha]

what is the difference between m ≡ m' [MOD 9] and ↑m' ≡ ↑m [ZMOD 9]

import Mathlib

open List
lemma rearrange_digits_diff_multiple_of_9 (m m' : ℕ)
    (h_perm : Nat.digits 10 m ~ Nat.digits 10 m') :
    m ≡ m' [MOD 9]  := by
      have h_m_sum : m ≡ (Nat.digits 10 m).sum [MOD 9] := by
        exact Nat.modEq_nine_digits_sum m
      have h_m'_sum : m' ≡ (Nat.digits 10 m').sum [MOD 9] := by
        exact Nat.modEq_nine_digits_sum m'
      have h_sum_eq : (Nat.digits 10 m).sum = (Nat.digits 10 m').sum := by
        exact Perm.sum_eq h_perm
      rw [← h_sum_eq] at h_m'_sum
      exact Nat.ModEq.trans h_m_sum (Nat.ModEq.symm h_m'_sum)
theorem rearrange (m m' : ℕ)
    (h_perm : Nat.digits 10 m ~ Nat.digits 10 m') :
    (9 ) ∣ (m : ℤ) - (m' : ℤ) := by

  rw [← @Int.modEq_iff_dvd]
  have h_nat_modeq : m ≡ m' [MOD 9] := by exact rearrange_digits_diff_multiple_of_9 m m' h_perm
  ```

[Kevin Buzzard]

They're mathematically equivalent (this will follow from theorems in the library), but formally one is a statement about naturals and the other is a statement about integers, one has the prime on the left and the other on the right etc, there are several formal differences.

[vxctyxeha]

thanks