mathlib

97bdf517 - chore(algebra/*): mark frozen files that have been ported to mathlib4 (#17039)

chore(algebra/*): mark frozen files that have been ported to mathlib4 (#17039) This is chiefly a proposal that we get started marking files as frozen, and a proposal for a specific format. Once we settle on what gets written here, we should add some CI that adds a special label to any PR modifying a frozen file. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>