no goals
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : a = 0
⊢ (fun x => x * a) '' [[b, c]] = [[b * a, c * a]]
simp [ha]
no goals
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : ¬a = 0
⊢ (fun x => x * a⁻¹) ⁻¹' [[b, c]] = (fun x => x / a) ⁻¹' [[b, c]]
simp only [div_eq_mul_inv]