Theorem exists_linearIndependent_algEquiv_apply

Modification history

2026-01-31 15:52
Mathlib/FieldTheory/Galois/NormalBasis.lean
chore(FieldTheory/Galois/NormalBasis): don't expose file (#34630) …
Deleted exists_linearIndependent_algEquiv_applyView on Github →
2025-09-27 09:23
Mathlib/FieldTheory/Galois/NormalBasis.lean
feat(FieldTheory/Galois): normal basis theorem (#27390) …
Added exists_linearIndependent_algEquiv_applyView on Github →