Zulip Chat Archive

Stream: triage

Topic: issue #11678: Typo in Mathlib.Condensed.Explicit doc


Violeta Hernández (Dec 12 2024 at 11:26):

This is a very simple issue just pointing out a possible typo, can someone verify if the suggested correction is correct and close this?

#11678

Kevin Buzzard (Dec 14 2024 at 00:05):

Why don't you make a PR?

Violeta Hernández (Dec 14 2024 at 01:10):

Well I don't actually know if this is a typo or not

Violeta Hernández (Dec 14 2024 at 01:10):

If it is then I'll make one

Kevin Buzzard (Dec 14 2024 at 01:27):

I think it is.


Last updated: May 02 2025 at 03:31 UTC