ZMod p to Nat

Stream: new members

[sky]

import Mathlib

open Nat ZMod
open Finset

example (p : ℕ) [Fact p.Prime] :
    ∏ x ∈ Finset.univ.erase (0 : ZMod p), x = ∏ x ∈ Ico 1 p, ↑x := by

  sorry

i might to prove this equation, how can i do, please help me (please do not use fermat little thm, i m trying to proving it and this is a little part of the proof)

[Terence Tao]

You basically need to set up a bijection, injection or equivalence between the two domains here. Several of the options in the loogle search below would get you started

[Terence Tao]

@loogle Finset.prod ?a ?b = Finset.prod ?c ?d

[loogle]

:search: Function.Bijective.prod_comp, Finset.prod_map, and 180 more

[Yiming Fu]

Using Finset.prod_nbij looks like a proper choice.