Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_algebraic_iff_is_integral'

Modification history

2022-02-02 13:59
src/ring_theory/algebraic.lean
refactor(ring_theory): clean up `algebraic_iff_integral` (#11773) …
Deleted is_algebraic_iff_is_integral'View on Github →
2020-12-30 23:15
src/ring_theory/algebraic.lean
feat(field_theory/algebraic_closure): algebraically closed fields have no nontrivial algebraic extensions (#5537)
Added is_algebraic_iff_is_integral'View on Github →