Theorem Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable

Modification history

2026-04-01 07:42

Mathlib/RingTheory/Smooth/Field.lean

chore(RingTheory/Smooth): remove fg condition for `Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable` (#37301)

Modified Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable View on Github →

2026-01-20 18:20

Mathlib/RingTheory/Smooth/Field.lean

feat(RingTheory): field extension over perfect fields are smooth (#32617)

Added Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable View on Github →