mathlib

40a0ac77 - chore(linear_algebra/finite_dimensional): change instance (#6713)

chore(linear_algebra/finite_dimensional): change instance (#6713) With the new instance `finite_dimensional K K` Lean can deduce the old instance automatically. I don not completely understand why it needs the new instance (`apply_instance` proves it), probably this is related to the order of unfolding `finite_dimensional` and applying `is_noetherian` instances.