Fin.prod_range

Stream: mathlib4

[Violeta Hernández]

Why do we have both docs#Finset.prod_range and docs#Fin.prod_univ_eq_prod_range ?

[Kevin Buzzard]

docs#Fin.prod_univ_eq_prod_range

[Kevin Buzzard]

Given that the proof is

@[to_additive]
theorem prod_range [CommMonoid β] {n : ℕ} (f : ℕ → β) :
    ∏ i ∈ Finset.range n, f i = ∏ i : Fin n, f i :=
  (Fin.prod_univ_eq_prod_range _ _).symm

it is clear that this was intentional, at least.

[Violeta Hernández]

Not sure if I agree with that given that both lemmas are in very different files

[Violeta Hernández]

(In particular, Fin.prod_range requires many more imports)

[Kevin Buzzard]

I mean the proof of one uses the other so they weren't added independently by people who didn't realise that the other one existed.

[Violeta Hernández]

Perhaps the proof was simply golfed during porting?

[Violeta Hernández]

Actually, this had a longer proof in Lean 3 apparently: https://github.com/leanprover-community/mathlib4/commit/f0a4e27ecde075e2061b26a8406ef588de283783#diff-53474c1bc0645f14175824ab090185307a25bcf6cc09e9d764c2287035f79008R36

[Violeta Hernández]

It was then golfed by @Yury G. Kudryashov in #4875

[Violeta Hernández]

So this all points to being an oversight

[Violeta Hernández]

The question now is: which theorem should stay?

[Yury G. Kudryashov]

Yes, I've noticed the duplication but golfed instead of properly deduplicating.