Zulip Chat Archive
Stream: general
Topic: Erratum for Mathematics in Lean
Martin C. Martin (Jan 31 2023 at 20:31):
In section 2.5. Proving Facts about Algebraic Structures, it looks like someone replaced "min" with "inf", and got a little carried away.
"analogous to inf and max " should be "analogous to min and max"
"keep the following dictionary in infd:" should be "keep the following dictionary in mind:"
Martin C. Martin (Jan 31 2023 at 20:32):
There are a few other examples later in that section too.
Patrick Massot (Jan 31 2023 at 20:43):
Fixed in https://github.com/avigad/mathematics_in_lean_source/commit/96f29addfae2c4971e5b006cfd1404c95e440758
Patrick Massot (Jan 31 2023 at 20:44):
@Jeremy Avigad it would be nice to deploy a build.
Jeremy Avigad (Jan 31 2023 at 20:58):
Done! Thanks to both of you for the fixes.
Last updated: Dec 20 2023 at 11:08 UTC