Commit 2026-10-21 08:37 eb6d361f

chore: modulize docs (#45107) This PR turns docs.lean and the two docs/ files (which only contain module docstrings, for inclusion in the docs page) into modules. Note that building docs warns that non-modules are not allowed due to mathlib's requiresModuleSystem := true lakefile setting. This only escapes CI because docs is never actually built by (mathlib) CI.