Commit 2026-02-25 14:16 d20aa7a3

View on Github →

chore: add theorem attributes, trivial theorems on orders of meromorphic functions (#35689) Add missing attributes @[to_fun] and missing trivial lemmas to aid proof automatisation.

Estimated changes

Modified Mathlib/Analysis/Meromorphic/Order.lean

added theorem meromorphicOrderAt_div

added theorem meromorphicOrderAt_id_sub_const

modified theorem meromorphicOrderAt_inv

modified theorem meromorphicOrderAt_mul

modified theorem meromorphicOrderAt_pow

added theorem meromorphicOrderAt_pow_id_sub_const

modified theorem meromorphicOrderAt_smul

modified theorem meromorphicOrderAt_zpow

added theorem meromorphicOrderAt_zpow_id_sub_const