Commit 2023-01-18 17:47 7c3780f6
View on Github →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.