Skip to content

Commit

Permalink
doc(AlgebraicIndependent): remove outdated TODO and add new (#9396)
Browse files Browse the repository at this point in the history
The TODO item was already completed as [IsTranscendenceBasis.isAlgebraic](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/AlgebraicIndependent.html#IsTranscendenceBasis.isAlgebraic). However, transcendence degree is nowhere to be found even though it appears in the tags.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
  • Loading branch information
3 people committed Jan 3, 2024
1 parent 7d58fa3 commit e23b087
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion Mathlib/RingTheory/AlgebraicIndependent.lean
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,8 @@ This file defines algebraic independence of a family of element of an `R` algebr
* [Stacks: Transcendence](https://stacks.math.columbia.edu/tag/030D)
## TODO
Prove that a ring is an algebraic extension of the subalgebra generated by a transcendence basis.
Define the transcendence degree and show it is independent of the choice of a
transcendence basis.
## Tags
transcendence basis, transcendence degree, transcendence
Expand Down

0 comments on commit e23b087

Please sign in to comment.