data.int.basic

Stream: general

[Johan Commelin]

Should data.int.basic depend on algebra.char_zero which depends on algebra.field which depends on... ?

[Gabriel Ebner]

It is certainly inconvenient. The import is only necessary for four lemmas, right?

[Chris Hughes]

The lemma in data.int.basic that depend on char_zero are all variants of cast being injective which could be moved to char_zero

[Chris Hughes]

I don't think it matters that much since they're all fairly low down in the hierarchy.

[Scott Morrison]

Removing the dependency does sounds reasonable. Getting data.int.basic done early is a good idea. It would be great if we had per file compilation times, and could see what the long pole was for compiling mathlib.

[Scott Morrison]

(Assuming excessive parallelism.)