split Mathlib/RingTheory/Int.lean

Stream: mathlib4

[Kim Morrison]

Would someone be interested in splitting Mathlib/RingTheory/Int.lean? It has some very basic results mixed in with some higher powered ones. As a consequence we have silly imports like Mathlib.GroupTheory.Perm.Fin knowing about LinearMap. (Indeed, a good test of the split of Mathlib/RingTheory/Int.lean would be adding assert_not_exists LinearMap there.)

[Ruben Van de Velde]

Do you mean Int/Basic.lean? I am interested, yeah, but don't want to stop anyone who's got time right now

[Kim Morrison]

I couldn't resist the temptation. #12341