See note [X]

Stream: mathlib4

[Kenny Lau]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Localization/Defs.html#IsLocalization.ringHom_ext says "See note [partially-applied ext lemmas]"; how do I see the note?

[Junyan Xu]

The mathlib3 docs page is here but I don't know if mathlib4 has a corresponding page.
The mathlib3 file containing the note is this but the corresponding Lean 4 file doesn't contain a library note.

[Michael Rothgang]

See also this previous discussion: #mathlib4 > library notes

[Michael Rothgang]

In short: I had a proposal for making the library notes display correctly, but got only lukewarm feedback (hence didn't pursue it further yet). I'm open to reviving my PR.

[Michael Rothgang]

There was also discussion about adding special syntax for references to library notes, but that part of the discussion didn't converge yet.

[Edward van de Meent]

also, this particular note hasn't been ported, see #10968

[Kenny Lau]

so currently they are no-op?

[Edward van de Meent]

(if it were, you should be able to #help note "foo" and see the relevant note displayed in the infoview)

[Eric Wieser]

This particular note has a paper written about it :)

[Edward van de Meent]

it does?

[Eric Wieser]

https://scholar.google.com/scholar?cluster=7582702216007405636&hl=en&as_sdt=2005&sciodt=0,5, I should probably upload to arxiv too

[Robin Carlier]

The ported note should include a link to the paper, once it’s on Arxiv.

[Eric Wieser]

The paper is on Zulip at chaining-extensionality.pdf in the meantime