feat(Algebra/GroupWithZero/Units/Lemmas): div_div_div_cancel_left' (#…

…6606) Co-authored-by: Moritz Firsching <firsching@google.com>
leanprover-community · Aug 16, 2023 · ee38ee9 · ee38ee9
1 parent 38c0722
commit ee38ee9
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean b/Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean
@@ -199,6 +199,9 @@ theorem div_helper (b : G₀) (h : a ≠ 0) : 1 / (a * b) * a = 1 / b := by
   rw [div_mul_eq_mul_div, one_mul, div_mul_right _ h]
 #align div_helper div_helper
 
+theorem div_div_div_cancel_left' (a b : G₀) (hc : c ≠ 0) : c / a / (c / b) = b / a := by
+  rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]
+
 end CommGroupWithZero
 
 section MonoidWithZero

diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Base.lean b/Mathlib/Analysis/SpecialFunctions/Log/Base.lean
@@ -102,10 +102,8 @@ theorem mul_logb {a b c : ℝ} (h₁ : b ≠ 0) (h₂ : b ≠ 1) (h₃ : b ≠ -
 #align real.mul_logb Real.mul_logb
 
 theorem div_logb {a b c : ℝ} (h₁ : c ≠ 0) (h₂ : c ≠ 1) (h₃ : c ≠ -1) :
-    logb a c / logb b c = logb a b := by
-  unfold logb
-  -- TODO: div_div_div_cancel_left is missing for `group_with_zero`,
-  rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ (log_ne_zero.mpr ⟨h₁, h₂, h₃⟩)]
+    logb a c / logb b c = logb a b :=
+  div_div_div_cancel_left' _ _ <| log_ne_zero.mpr ⟨h₁, h₂, h₃⟩
 #align real.div_logb Real.div_logb
 
 section BPosAndNeOne