Finiteness of subalgebra of algebraic extensions of F_p

Stream: Is there code for X?

[Chris Hughes]

I'm trying to prove that a finitely generated subsemiring of an algebraic extension of $\mathbb{F}_p$ is finite. For this I think I need two facts.

1) finitely generated subalgebras of algebraic extensions are finite dimensional as a vector space
2) finite dimensional vector spaces over finite fields are finite

I think we must have both of these somewhere

[Eric Rodriguez]

docs#finite_dimensional.fintype_of_fintype for 2

[Riccardo Brasca]

For the first one you can use something like docs#power_basis.finite_dimensional

[Riccardo Brasca]

(if the extension is generated by a single element)

[Eric Rodriguez]

what about docs#is_noetherian.iff_fg?

[Chris Hughes]

Thanks. I've proved the lemma now.

[Chris Hughes]

That was the very last sorry in Ax-Grothendieck by the way so when I send the proof to @Joseph Hua he should have a full proof of Ax-Grothendieck

[Johan Commelin]

That's cool! Congrats!

[Joseph Hua]

It's incorporated wooo