Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-22 20:15 72c20fab

View on Github →

feat(analysis/special_functions/exp_log): Classify when log is zero (#9815) Classify when the real log function is zero.

Estimated changes

added theorem real.log_eq_zero