Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-13 17:03 8eca2934

View on Github →

feat(field_theory): more general algebra _ (algebraic_closure k) instance (#8658) For example, now we can take a field extension L / K and map x : K into the algebraic closure of L.

Estimated changes