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:33:19 +01:00
parent 9ebb1c5215
commit 62abf21cfd
1 changed files with 0 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Nevanlinna/stronglyMeromorphicAt.lean
View File

@ -347,7 +347,6 @@ theorem makeStronglyMeromorphic_id
by_contra hn
rw [hn] at this
tauto
· exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz