tensor product L(x)[K] commutes with arbitrary products if L/K finite

ImperialCollegeLondon / FLT

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Apache License 2.0

262 stars 48 forks source link

tensor product L(x)[K] commutes with arbitrary products if L/K finite #239

Open kbuzzard opened 3 days ago

kbuzzard commented 3 days ago

This is the missing sorry in ProdAdicCompletions.baseChangeEquiv. The point is that L=K^n so L (x)[K] (\prod_i A_i) = \prod_i A_i^n. Note that it's not true that tensor products commute with infinite products in general.