mathlib

3e4d6aa3 - feat(algebra/algebra/basic): add instances `char_zero.no_zero_smul_divisors_int`, `char_zero.no_zero_smul_divisors_nat` (#14395)

feat(algebra/algebra/basic): add instances `char_zero.no_zero_smul_divisors_int`, `char_zero.no_zero_smul_divisors_nat` (#14395) The proofs are taken from #14338 where a specific need for these arose Aside from the new instances, nothing else has changed; I moved the `no_zero_smul_divisors` section lower down in the file since the new instances need the `algebra ℤ R` structure carried by a ring `R`.