Theorem exists_linearIndependent_algEquiv_apply_of_infinite

Modification history

2026-01-31 15:52
Mathlib/FieldTheory/Galois/NormalBasis.lean
chore(FieldTheory/Galois/NormalBasis): don't expose file (#34630) …
Added exists_linearIndependent_algEquiv_apply_of_infiniteView on Github →