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

Update logabs.lean

This commit is contained in:
Stefan Kebekus 2024-04-25 19:16:21 +02:00
parent cbe98c404b
commit 98efcf9f87
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
nevanlinna/logabs.lean
View File

@ -46,7 +46,7 @@ lemma logAbsXX : ∀ z : ℂ, z ≠ 0 → Real.log (Complex.abs z) = (1 / 2) * C
rw [t₃] rw [t₃]
rw [Complex.normSq_eq_conj_mul_self] rw [Complex.normSq_eq_conj_mul_self]
have : conj z ≠ 0 := by have t₄ : conj z ≠ 0 := by
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr z₁Hyp exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr z₁Hyp
let XX := Complex.log_mul_eq_add_log_iff this z₁Hyp let XX := Complex.log_mul_eq_add_log_iff this z₁Hyp