Theorem exists_linearIndependent_algEquiv_apply

Modification history

2025-09-27 09:23
Mathlib/FieldTheory/Galois/NormalBasis.lean
feat(FieldTheory/Galois): normal basis theorem (#27390) …
Added exists_linearIndependent_algEquiv_applyView on Github →