Commit 2026-01-31 15:52 953451db

chore(FieldTheory/Galois/NormalBasis): don't expose file (#34630) Remove the @[expose] public section at the top of the file, instead marking each public theorem individually. normalBasis is completely characterized by normalBasis_apply, and has no interesting defeqs, so it is not exposed.