algebra.has_scalar causing problems

Stream: general

[Chris Hughes]

Should we change the priority or get rid of algebra.has_scalar? It causes this search to fail. Changing the priority to 999 fixes it.

import data.matrix data.rat.basic ring_theory.algebra

local attribute [instance, priority 1000] algebra.has_scalar

instance X {m : ℕ} : has_scalar ℚ (matrix (fin m) (fin m) ℚ) := by apply_instance

[Chris Hughes]

I think perhaps it might be a good idea to split files up a bit more, to avoid too many imports. Every now and then, there's a lemma that doesn't belong anywhere, so an import gets added to a file. I personally wouldn't mind just making a new file for that lemma, if it means reducing unnecessary imports, which slow down type class inference.

[Floris van Doorn]

I don't like the idea of having to be careful with imports because otherwise type class inference will fail. If type class inference fails because we have to many instances, we need to declare fewer instances. Your suggestion is also just postponing the problem: at some point we want to import enough files to cause a problem anyway.

[Floris van Doorn]

I am generally happy to be careful with imports for other reasons (e.g. unnecessary recompilations after you change a basic file), but I don't like files with just 1 or 2 lemmas: it will also make it harder to find these lemmas.

[Floris van Doorn]

As a concrete example, PR #1294 adds the lemma stating that the multiplicity of prime p in a finite product of numbers is the sum of the multiplicities.

lemma finset.prod {β : Type*} [decidable_eq β] {p : α} (hp : prime p) (s : finset β) (f : β → α) :
  multiplicity p (s.prod f) = s.sum (λ x, multiplicity p (f x))

Should that be in a file other than multiplicity, so that multiplicitydoesn't have to import big_operators? I'm still quite often searching for lemmas in the old-fashioned way of scrolling (and ctrl+F-ing) through files, and it will make it harder to find that.

I also added some other imports on #1294 for which I feel a lot less strongly about. Please review that PR with suggestions of how to do it otherwise.

[Chris Hughes]

That I'm okay with, since most of the stuff using prime numbers will also using big operators.

Stuff like ring_theory.algebra importing tensor products, complex numbers, and multivariate polynomials, which are then imported by finite dimensional vector spaces is a bit much. I need all this just to prove A * B = 1 -> B * A = 1 for rational matrices.

[Kevin Buzzard]

This does seem a bit ridiculous. However I guess there are other computer programs which also have this problem so presumably the CS guys have got some ideas about how to deal with it.