ι : Type ?u.7675134
𝕜 : Type ?u.7675137
E : Type u_1
F : Type ?u.7675143
A : Type ?u.7675146
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
⊢ IntervalIntegrable (fun x => f (-1 * x)) volume (a / -1) (b / -1) ↔
    IntervalIntegrable (fun x => f (-x)) volume (-a) (-b)
ι : Type ?u.7675134
𝕜 : Type ?u.7675137
E : Type u_1
F : Type ?u.7675143
A : Type ?u.7675146
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
⊢ IntervalIntegrable f volume a b ↔ IntervalIntegrable (fun x => f (-x)) volume (-a) (-b)
rw [← comp_mul_left_iff (neg_ne_zero.2 one_ne_zero)]
no goals
ι : Type ?u.7675134
𝕜 : Type ?u.7675137
E : Type u_1
F : Type ?u.7675143
A : Type ?u.7675146
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
⊢ IntervalIntegrable (fun x => f (-1 * x)) volume (a / -1) (b / -1) ↔
    IntervalIntegrable (fun x => f (-x)) volume (-a) (-b)
simp [div_neg]