Commit 2025-07-04 07:31 389ef58c

View on Github →

feat: compute trailing coefficients of factorized rational functions (#26141) This PR continues the work from #25523. Original PR: https://github.com/leanprover-community/mathlib4/pull/25523

Estimated changes

Modified Mathlib/Analysis/Meromorphic/FactorizedRational.lean

added theorem Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt

added theorem Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational

added theorem Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational_off_support

added theorem MeromorphicOn.log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles

added theorem MeromorphicOn.meromorphicTrailingCoeffAt_extract_zeros_poles

Modified Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean

added theorem meromorphicTrailingCoeffAt_const

added theorem meromorphicTrailingCoeffAt_id_sub_const

added theorem meromorphicTrailingCoeffAt_prod