Theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_fg

Modification history

2026-01-20 18:20
Mathlib/FieldTheory/SeparablyGenerated.lean
feat(RingTheory): field extension over perfect fields are smooth (#32617)
Deleted exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_fgView on Github →
2025-12-05 11:03
Mathlib/FieldTheory/SeparablyGenerated.lean
feat(FieldTheory): fg extension over perfect field is separably generated (#30998)
Added exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_fgView on Github →