Strange condition on nat_mul_inj'

Stream: mathlib4

[Jz Pan]

docs#nat_mul_inj' requires NoZeroDivisors R and CharZero R. But I think it only requires NoZeroSMulDivisors ℕ R. Is it true?

[Yaël Dillies]

Yes: docs#nsmul_right_inj

[Jz Pan]

I've checked that IsAddTorsionFree instance cannot be synthesized correctly if without importing certain files. For example in here https://github.com/leanprover-community/mathlib4/pull/22620#discussion_r2117890558

So it seems that nsmul_right_inj requires more import than nat_mul_inj'.

[Yaël Dillies]

Aha, we should definitely fix this!

[Jz Pan]

(deleted)