a / b / a = b⁻¹

Stream: Is there code for X?

[Eric Wieser]

Do we have the with_zero version of docs#div_div_cancel_left?

lemma div_div_cancel_left' {G₀} [comm_group_with_zero G₀] (a b : G₀) (ha : a ≠ 0) :
  a / b / a = b⁻¹ :=
by rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, mul_inv_cancel ha, one_mul]

[Eric Wieser]

#18421