Commit 2021-12-08 22:28 bcd9a745
View on Github →refactor(data/complex/is_R_or_C): finite_dimensional.proper_is_R_or_C is not an instance anymore (#10629)
This instance caused a search for [finite_dimensional ?x E] with an unknown ?x. Turn it into a lemma and add haveI to some proofs. Also add an instance for K ∙ x.