Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subalgebra.inv_mem_of_algebraic

Modification history

2020-11-04 16:04

src/ring_theory/algebraic.lean

feat(ring_theory/algebraic): if `L / K` is algebraic, then the subalgebras are fields (#4903)

Added subalgebra.inv_mem_of_algebraic View on Github →