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.