The L-algebra map L tensor K_v -> prod_{w|v} L_w is continuous

[kbuzzard]

The K-algebra map K_v -> prod_{w|v} L_w is continuous, and L/K is finite, and L tensor K_v has the module topology, so this issue is just a case of figuring out why tensoring with L preserves continuity.

[erdOne]

This follows immediately from leanprover-community/mathlib4#19515 I think

[kbuzzard]

This is in FLT now. Do you want to try your luck @erdOne ?

[erdOne]

Its #251