Commit 2021-08-23 17:55 700effae
View on Github →feat(ring_theory/localization): the algebraic elements over Frac(R) are those over R (#8826)
We had this lemma for L / K is algebraic iff L / A is, but now we also have it elementwise!
feat(ring_theory/localization): the algebraic elements over Frac(R) are those over R (#8826)
We had this lemma for L / K is algebraic iff L / A is, but now we also have it elementwise!