You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
There we would like in "See library note [bundled maps over different rings]." for "bundled maps over different rings" to hyperlink to the doc-comment in Mathlib.GroupTheory.GroupAction.Defs, and moreover for the library_note in that file to actually be rendered on the documentation page! (It should come just above VAddCommClass.)
The text was updated successfully, but these errors were encountered:
See https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Basis.html#Basis.constr for an example.
There we would like in "See library note [bundled maps over different rings]." for "bundled maps over different rings" to hyperlink to the doc-comment in Mathlib.GroupTheory.GroupAction.Defs, and moreover for the
library_note
in that file to actually be rendered on the documentation page! (It should come just aboveVAddCommClass
.)The text was updated successfully, but these errors were encountered: