Prove that a^2 | a for a \in \Z

Stream: Is there code for X?

[Mattia Bottoni]

Hi everybody :)
I am trying to prove the following statement:
Recall that x|y means there exists an integer k, such that y = kx. Show that if a is an integer and a^2|a, then a ∈ {0, 1,−1}.

This is what I have got so far:
example (a : ℤ) : (a ^ 2 ∣ a) → ((a = -1) ∨ (a = 1) ∨ (a = 0)) := by
intro h
by_cases h_nonzero : a ≠ 0
obtain ⟨k, hk⟩ := h
sorry
done

I would need some tactic that tells me that the only divisors of one in the integer are 1 and -1.
Can you help me out?
Thank you all in advance
Matt

[Mario Carneiro]

you don't need a tactic, you need a theorem that says that

[Mario Carneiro]

docs#Int.eq_one_of_dvd_one

[Mattia Bottoni]

I applied the theorem but now I am stuck because I would need to prove that 0 \leq a.

a2diva.png

Output-a2diva.png

[Ruben Van de Velde]

#mwe , please

[Mattia Bottoni]

import Mathlib.Tactic
example (a : ℤ) : (a ^ 2 ∣ a) → ((a = -1) ∨ (a = 1) ∨ (a = 0)) := by
intro h
by_cases h2 : a = 0
right
right
exact h2
by_cases h1 : a = -1
left
exact h1
right
left
apply Int.eq_one_of_dvd_one

done

[Scott Morrison]

#backticks

[Mattia Bottoni]

import Mathlib.Tactic
example (a : ℤ) : (a ^ 2 ∣ a) → ((a = -1) ∨ (a = 1) ∨ (a = 0)) := by
intro h
by_cases h2 : a = 0
right
right
exact h2
by_cases h1 : a = -1
left
exact h1
right
left
apply Int.eq_one_of_dvd_one

done

Sorry, I did not know this.

[Riccardo Brasca]

Well, now you have a goal 0 ≤ a, that is not true in general, so you took a wrong turn.

[Riccardo Brasca]

My suggestion is to write down a precise mathematical proof (with pen and paper) and then try to formalize it.

[Riccardo Brasca]

For example,

import Mathlib.Tactic

example (a : ℤ) : (a ^ 2 ∣ a) → ((a = -1) ∨ (a = 1) ∨ (a = 0)) := by
  rintro ⟨k, hk⟩
  by_cases h0 : a = 0
  · simp [h0]
  · rw [pow_two, mul_assoc] at hk
    rw [← or_assoc]
    left
    refine or_comm.1 (Int.isUnit_iff.1 (isUnit_of_dvd_one ⟨k, ?_⟩))
    exact (Int.eq_one_of_mul_eq_self_right h0 hk.symm).symm

works. The key points are docs#Int.eq_one_of_mul_eq_self_right (I found it via exact?) that simplifies the a and docs#Int.isUnit_iff (I found it guessing the name) that tells you what are the units if ℤ.

[Riccardo Brasca]

I am a little surprised we dont have Int.dvd_one_iff...

[Gareth Ma]

Riccardo Brasca said:

I am a little surprised we dont have Int.dvd_one_iff...

Probably considered a duplicate of isUnit_iff, but it's definitely good to have.

[Mario Carneiro]

it's not a duplicate of isUnit_iff, but it is a one liner using it

[Mario Carneiro]

theorem Int.dvd_one_iff (a : ℤ) : a ∣ 1 ↔  a = 1 ∨ a = -1 := by
  rw [← isUnit_iff_dvd_one, Int.isUnit_iff]

[Mattia Bottoni]

Thank you so much for your help!

I will definitely have a look at the two docs you sent @Riccardo Brasca