no goals
ι : Type ?u.38496
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.38508
δ : Type ?u.38511
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f (x / y) = ↑f (y / x)
rw [← inv_div, map_inv_eq_map]