refactor(Algebra/Polynomial/Laurent): use Int.ofNat.inj

[mo271]

trafficstars

---

[mo271]

Not sure if we want to have a special name for a theorem of type Function.Injective Int.ofNat which is just Int.ofNat.inj with explicit arguments. If yes, what would be a good name and place for it?

[mo271]

Perhaps this is a use case for using alias?

[Ruben-VandeVelde]

Actually, I do think we should have the Injective lemma as well

[mo271]

Actually, I do think we should have the Injective lemma as well

What would be a good name and place for it?

[Ruben-VandeVelde]

Int.ofNat_injective, and near Int.natCast_inj in Data.Int.Defs, perhaps

[mo271]

Int.ofNat_injective, and near Int.natCast_inj in Data.Int.Defs, perhaps

done

[urkud]

I'm going to test if Nat.cast_injective works better in these rws. UPD: In 1 case it doesn't help (why do we need erw there?) ; in other case, expr uses Nat.cast, so I rewrote it in terms of Nat.cast_injective.

[urkud]

Thanks! Once CI is happy, please merge this PR using bors r+ bors d+

[mathlib-bors[bot]]

:v: mo271 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mo271]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style