Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 09:48 1faf964e

View on Github →

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

Estimated changes

Modified src/ring_theory/algebraic_independent.lean

added theorem algebraic_independent.aeval_comp_mv_polynomial_option_equiv_polynomial_adjoin

added theorem algebraic_independent.algebra_map_aeval_equiv

added def algebraic_independent.mv_polynomial_option_equiv_polynomial_adjoin

added theorem algebraic_independent.option_iff

added theorem exists_is_transcendence_basis

added theorem is_transcendence_basis.is_algebraic