ι : Type ?u.34747
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.34759
δ : Type ?u.34762
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f (x * y⁻¹) ≤ ↑f x + ↑f y⁻¹
ι : Type ?u.34747
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.34759
δ : Type ?u.34762
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f (x / y) ≤ ↑f x + ↑f y
rw [div_eq_mul_inv, ← map_inv_eq_map f y]
no goals
ι : Type ?u.34747
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.34759
δ : Type ?u.34762
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f (x * y⁻¹) ≤ ↑f x + ↑f y⁻¹
exact map_mul_le_add _ _ _