Commit 2025-01-26 04:59 771b149b

View on Github →

feat: log (x / x) = 0 (#21056) From PFR

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

added theorem Complex.arg_div_self

modified theorem Complex.arg_one

Modified Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

added theorem Complex.log_div_self

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

added theorem Real.log_div_self