mathlib

7c3780f6 - feat(algebra/triv_sq_zero_ext): lemmas about pow, and ring structure (#18199)

feat(algebra/triv_sq_zero_ext): lemmas about pow, and ring structure (#18199) `snd_pow : snd (x ^ n) = n • x.fst ^ n.pred • x.snd` captures the use of dual numbers in automatic differentiation. Also add myself to the authors, since I've done some work on this file in the past.