Commit 2021-06-11 21:18 64d453ee

feat(ring_theory/adjoin/basic): add subalgebra.fg_prod (#7811) We add subalgebra.fg_prod: the product of two finitely generated subalgebras is finitely generated. A mathematical remark: the result is not difficult, but one needs to be careful. For example, algebra.adjoin_eq_prod is false without adding (1,0) and (0,1) by hand to the set of generators. Moreover, linear_map.inl and linear_map.inr are not ring homomorphisms, so it seems difficult to mimic the proof for modules. A better mathematical proof is to take surjections from two polynomial rings (in finitely many variables) and considering the tensor product of these polynomial rings, that is again a polynomial ring in finitely many variables, and build a surjection to the product of the subalgebras (using the universal property of the tensor product). The problem with this approach is that one needs to know that the tensor product of polynomial rings is again a polynomial ring, and I don't know well enough the API fort the tensor product to prove this.