issue !4#11678: Typo in Mathlib.Condensed.Explicit doc

Stream: triage

[Random Issue Bot]

Today I chose issue #11678 for discussion!

Typo in Mathlib.Condensed.Explicit doc
Created by @Matt Diamond (@mattdiamond) on 2024-03-25
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

This issue is still relevant, the module docstring for Mathlib/Condensed/Explicit.lean claims that Condensed.ofSheafStonean does two different things, but this should not be an issue, this should be a PR.

[Random Issue Bot]

Today I chose issue #11678 for discussion!

Typo in Mathlib.Condensed.Explicit doc
Created by @Matt Diamond (@mattdiamond) on 2024-03-25
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

@Dagur Asgeirsson indeed the module docstring for https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Condensed/Explicit.lean gives two different descriptions of Condensed.ofSheafStonean.

[Dagur Asgeirsson]

Thanks for the ping, I’ll fix this

[Dagur Asgeirsson]

#32478