no goals
ι : Type ?u.127014
R : Type ?u.127017
R' : Type ?u.127020
E : Type u_1
F : Type ?u.127026
G : Type ?u.127029
inst✝² : AddGroup E
inst✝¹ : AddGroup F
inst✝ : AddGroup G
p q : NonarchAddGroupSeminorm E
⊢ ↑p.toZeroHom = ↑p
rfl