kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update stronglyMeromorphicAt.lean

This commit is contained in:
Stefan Kebekus 2024-11-14 15:54:21 +01:00
parent ccfc457c48
commit f22cea20a0
1 changed files with 0 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Nevanlinna/stronglyMeromorphicAt.lean
View File

@ -357,8 +357,6 @@ theorem StronglyMeromorphicAt.decompose
∧ (g z₀ ≠ 0) ∧ (g z₀ ≠ 0)
∧ (f = (fun z ↦ (z-z₀) ^ (h₁f.meromorphicAt.order.untop h₂f)) * g) := by ∧ (f = (fun z ↦ (z-z₀) ^ (h₁f.meromorphicAt.order.untop h₂f)) * g) := by
let n := - h₁f.meromorphicAt.order.untop h₂f
let g₁ := (fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)) * f let g₁ := (fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)) * f
let g₁₁ := fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f) let g₁₁ := fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)
have h₁g₁₁ : MeromorphicAt g₁₁ z₀ := by have h₁g₁₁ : MeromorphicAt g₁₁ z₀ := by