feat(ring_theory/tensor_product): Supremum of finite dimensional subalgebras (#10922)
feat(ring_theory/tensor_product): Supremum of finite dimensional subalgebras (#10922)

The supremum of finite dimensional subalgebras is finite dimensional.





leanprover-community/mathlib,leanprover-community/mathlib