Ausente no Mathlib v4.15 e no master (verificar de novo antes de começar). É O pré-requisito do próximo grande arco (expansão de caracteres em acoplamento forte). Candidato natural a colaboração com a comunidade via Zulip.
Aberto pelo Fable no encerramento da janela (2026-07-13); contexto completo em docs/legacy/.
Ausente no Mathlib v4.15 e no master (verificar de novo antes de começar). É O pré-requisito do próximo grande arco (expansão de caracteres em acoplamento forte). Candidato natural a colaboração com a comunidade via Zulip.
Aberto pelo Fable no encerramento da janela (2026-07-13); contexto completo em docs/legacy/.