mathlib

81207e09 - feat(algebra/triv_sq_zero_ext): trivial square-zero extension (#5109)