Zulip Chat Archive

Stream: general

Topic: A simple version of Finset.prod_image

Adam Kurkiewicz (Dec 01 2024 at 09:49):

I need to manipulate a prod over a Finset into an image + a prod using the identity function. I need this further on to prove that the images of two Finsets are equal. The Mathlib function Finset.prod_image is almost what I need, but not quite, and I don't think I can use it.

Any pointers?

That's the mwe:

import Mathlib

lemma finset_image_prod (p : ℕ) (pprime : p.Prime) (A : Finset ℤ) :
    (A.image (λ (x : ℤ) => (x : ZMod p))).prod (λ x => x) = A.prod (λ (x : ℤ) => (x : (ZMod p))) := by
  have : ∀ x ∈ A, ∀ y ∈ A, (fun x ↦ (x : ZMod p)) x = (fun x ↦ (x : ZMod p)) y → x = y := by
    sorry
  have := @Finset.prod_image (ZMod p) (ZMod p) ℤ (λ x => x) _ _ A (λ x => x) this
  exact this

Kevin Buzzard (Dec 01 2024 at 09:55):

Are you asking how to prove that if two integers are equal mod p then they're equal? This is false (for example 0 and p are equal mod p). Sorry if I've misunderstood.

Kevin Buzzard (Dec 01 2024 at 10:00):

So for example if your original set is {2,2+p}, it has product 4+2p with image 4 mod p, but the image of the set mod p is just {2 mod p} with product 2 mod p.

Adam Kurkiewicz (Dec 01 2024 at 10:00):

No, the question is about turning a prod over finset using (x : ℤ) => (x : ZMod p) into an image over that finset (x : ℤ) => (x : ZMod p) and then a prod using the identity function x => x

Kevin Buzzard (Dec 01 2024 at 10:01):

Right but reduction mod p isn't injective so I think what you're claiming is false because the finset can degenerate

Adam Kurkiewicz (Dec 01 2024 at 10:01):

I believe that this is true:

import Mathlib

lemma finset_image_prod (p : ℕ) (pprime : p.Prime) (A : Finset ℤ) :
    (A.image (λ (x : ℤ) => (x : ZMod p))).prod (λ x => x) = A.prod (λ (x : ℤ) => (x : (ZMod p))) := by
  sorry