Little.Basic

This file provides Fermat's little theorem.

Results

• mod_add_pow : if p is prime then (m + n)ᵖ ≡ mᵖ + nᵖ [MOD p]
• mod_pow_Fermat: if p is prime then nᵖ ≡ n [MOD p]

Notes

You should use Nat.ModEq.pow_totient instead of mod_pow_Fermat.

theorem mod_add_pow {p m n : ℕ} (hp : Nat.Prime p) : (m + n) ^ p ≡ m ^ p + n ^ p [MOD p]

theorem mod_pow_Fermat {p n : ℕ} (hp : Nat.Prime p) : n ^ p ≡ n [MOD p]

Fermat's little theorem