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 14:08:06 +01:00
parent 89abb9190f
commit 1a14bbbdd6
1 changed files with 6 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
Nevanlinna/stronglyMeromorphicAt.lean
View File

@ -392,14 +392,13 @@ theorem StronglyMeromorphicAt.decompose
have h₁g : StronglyMeromorphicAt g z₀ := by have h₁g : StronglyMeromorphicAt g z₀ := by
exact StronglyMeromorphicAt_of_makeStronglyMeromorphic h₁g₁ exact StronglyMeromorphicAt_of_makeStronglyMeromorphic h₁g₁
have h₂g : h₁g.meromorphicAt.order = 0 := by have h₂g : h₁g.meromorphicAt.order = 0 := by
rw [← h₁g₁.order_congr (m₂ h₁g₁)]
exact h₂g₁
sorry
constructor constructor
· apply analytic · apply analytic
· sorry · rw [h₂g]
· exact h₁g · exact h₁g
· constructor · constructor
· sorry · exact (order_eq_zero_iff h₁g).mp h₂g
· sorry ·
sorry