Commit 2025-12-20 21:16 fb469c76

View on Github →

chore: use the to_fun attribute (#32231) Reduce code duplication using the to_fun attribute. This is not exhaustive, neither does it constitute an endorsement "we always want to generate the applied form of a lemma".

Estimated changes

modified theorem AnalyticAt.add
deleted theorem AnalyticAt.fun_add
deleted theorem AnalyticAt.fun_const_smul
deleted theorem AnalyticAt.fun_inv
deleted theorem AnalyticAt.fun_mul
deleted theorem AnalyticAt.fun_neg
deleted theorem AnalyticAt.fun_pow
deleted theorem AnalyticAt.fun_smul
deleted theorem AnalyticAt.fun_sub
deleted theorem AnalyticAt.fun_zpow
deleted theorem AnalyticOn.fun_inv
deleted theorem AnalyticOn.fun_pow
deleted theorem AnalyticOn.fun_zpow
deleted theorem AnalyticOnNhd.fun_inv
deleted theorem AnalyticOnNhd.fun_pow
deleted theorem AnalyticOnNhd.fun_zpow
deleted theorem AnalyticWithinAt.fun_inv
deleted theorem AnalyticWithinAt.fun_pow
deleted theorem AnalyticWithinAt.fun_zpow
deleted theorem MeromorphicAt.fun_add
deleted theorem MeromorphicAt.fun_div
deleted theorem MeromorphicAt.fun_inv
deleted theorem MeromorphicAt.fun_mul
deleted theorem MeromorphicAt.fun_neg
deleted theorem MeromorphicAt.fun_pow
deleted theorem MeromorphicAt.fun_sub
deleted theorem MeromorphicAt.fun_zpow
modified theorem MeromorphicOn.add
modified theorem MeromorphicOn.div
deleted theorem MeromorphicOn.fun_add
deleted theorem MeromorphicOn.fun_div
deleted theorem MeromorphicOn.fun_inv
deleted theorem MeromorphicOn.fun_mul
deleted theorem MeromorphicOn.fun_neg
deleted theorem MeromorphicOn.fun_pow
deleted theorem MeromorphicOn.fun_sub
deleted theorem MeromorphicOn.fun_zpow
modified theorem MeromorphicOn.inv
modified theorem MeromorphicOn.mul
modified theorem MeromorphicOn.neg
modified theorem MeromorphicOn.pow
modified theorem MeromorphicOn.sub
modified theorem MeromorphicOn.zpow