Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-30 23:15 9c46cadc

View on Github →

feat(field_theory/algebraic_closure): algebraically closed fields have no nontrivial algebraic extensions (#5537)

Estimated changes

Modified src/field_theory/algebraic_closure.lean

added theorem is_alg_closed.algebra_map_surjective_of_is_algebraic

added theorem is_alg_closed.algebra_map_surjective_of_is_integral

Modified src/ring_theory/algebraic.lean

added theorem is_algebraic_iff_is_integral'