Zulip Chat Archive

Stream: Polynomial Freiman-Ruzsa conjecture

Topic: independence file

Floris van Doorn (Nov 22 2023 at 11:39):

Can someone that knows the probability theory library (@Rémy Degenne ?) skim over this file and see if there is anything that is already in mathlib or not stated properly?

Floris van Doorn (Nov 22 2023 at 11:40):

(ignore the first lemma Function.update_of_eq, I'm removing that)

Rémy Degenne (Nov 22 2023 at 21:50):

I'll have a look tomorrow.

Last updated: Dec 20 2023 at 11:08 UTC