Skip to content

chore: even more module system fixes and refinements from Mathlib porting #14056

chore: even more module system fixes and refinements from Mathlib porting

chore: even more module system fixes and refinements from Mathlib porting #14056

Backport

succeeded Oct 15, 2025 in 3s