feat(analysis/special_functions/exp_log): added log_div (#6196)

`∀ x y : ℝ, x ≠ 0 → y ≠ 0 → log (x / y) = log x - log y`
leanprover-community · Feb 12, 2021 · 254c3ee · 254c3ee
1 parent a5ccba6
commit 254c3ee
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/analysis/special_functions/exp_log.lean b/src/analysis/special_functions/exp_log.lean
@@ -411,6 +411,10 @@ lemma log_mul (hx : x ≠ 0) (hy : y ≠ 0) : log (x * y) = log x + log y :=
 exp_injective $
 by rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]
 
+lemma log_div (hx : x ≠ 0) (hy : y ≠ 0) : log (x / y) = log x - log y :=
+exp_injective $
+by rw [exp_log_eq_abs (div_ne_zero hx hy), exp_sub, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_div]
+
 @[simp] lemma log_inv (x : ℝ) : log (x⁻¹) = -log x :=
 begin
   by_cases hx : x = 0, { simp [hx] },