Zulip Chat Archive
Stream: mathlib4
Topic: port ConditionalExpectation.Basic !4#4898
Scott Morrison (Jun 12 2023 at 01:25):
This is a massive file, with many errors! I just fixed a bunch of errors.
Could we consider refactoring the file in mathlib3 into smaller pieces? @Rémy Degenne?
Rémy Degenne (Jun 12 2023 at 07:49):
Done in #19177
Jeremy Tan (Jun 17 2023 at 12:25):
This file (in its current, reduced form) is now awaiting review
Last updated: May 02 2025 at 03:31 UTC