[Merged by Bors] - feat(algebra/triv_sq_zero_ext): trivial square-zero extension

[kckennylau]

---

[jcommelin]

I'm afraid that the abbreviation tsze will not really scale. Would you mind spelling it out completely?
It's ok to use local notation to keep this file short and readable.
But outside this file, I think tsze would harm readability.

Apart from that LGTM

[kckennylau]

so trivial_square_zero_extension? won't this be a bit long?

[jcommelin]

How about a compromise? triv_sq_zero_ext? Most people can guess what that means, where as with tsze they cannot.
It's longer, hence I suggest that people use local notation if they need this a lot. But if you don't need it a lot, then it will be very helpful to know what this tsze actually is. Of course you can hover (if you are in an editor), but that's not something I want to rely on.
So I would default to longer and readable names, and then use local notation to make it shorter.

[jcommelin]

Thanks 🎉

bors merge

[jcommelin]

bors r-

[bors]

Canceled.

[jcommelin]

Oops, @kckennylau would you mind changing the filename as well?

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests
• Lint style