Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_independent.algebra_map_aeval_equiv

Modification history

2021-10-04 09:48

src/ring_theory/algebraic_independent.lean

feat(ring_theory/algebraic_independent): Existence of transcendence bases and rings are algebraic over transcendence basis (#9377)

Added algebraic_independent.algebra_map_aeval_equiv View on Github →