Mathematics in Lean, CRT - Notation confusion

Stream: new members

[Tainnor]

Mathematics in Lean (section 8.2.2) states a version of the Chinese Remainder Theorem as follows:

example {ι : Type*} [Fintype ι] (a : ι → ℕ) (coprime : ∀ i j, i ≠ j → (a i).Coprime (a j)) :
    ZMod (∏ i, a i) ≃+* ∀ i, ZMod (a i)

I am confused by the usage of ∀ in ∀ i, ZMod (a i) . Apparently, changing it to Π doesn't change the type - at least it still compiles with the same proof. Is this some sort of implicit way of writing a product?

[Mitchell Lee]

I believe that ∀ and Π mean exactly the same thing.

[A.]

The human convention is to write ∀ only in Props so a PR to change this would probably be well received.

[Patrick Massot]

This is indeed the same thing to Lean and obviously a typo in the context of MIL. In my defense this typo is a straight copy-paste from Mathlib so PRs to both MIL and Mathlib are welcome. In defense of Mathlib, note that in the early days of Lean 4 we didn’t have the nice notation because Leo decided it was useless to have this redundant notation in core Lean. But since he also first decided users would have the power to define such notations, we restored it.

[Patrick Massot]

Be careful when you fix the typo: there are many symbols that look similar. The correct statement

ZMod (∏ i, a i) ≃+* Π i, ZMod (a i)

features two different Pi-like symbols that bad fonts won’t make easy to distinguish.

[Patrick Massot]

I suddenly had a bad feeling about this story, and it has just been confirmed by git blame: I also authored the Mathlib version. My defense still stands, but requires a bit of schizophrenia.

[Tainnor]

Thanks for explaining. I didn't find it intuitive at first that they mean the same thing, although it makes a certain amount of sense once I think about it.

I made a PR for mathematics-in-lean: https://github.com/avigad/mathematics_in_lean_source/pull/193
I don't have write permissions for mathlib, otherwise I would have made one there too (it's my understanding that one shouldn't make PRs from forks).

[Michael Rothgang]

(This understanding is correct; mathlib's continuous integration requires running from not-a-fork.)