X : Type u_1
a b : FreeAbelianGroup X
⊢ (↑toFinsupp a + ↑toFinsupp b).support ⊆ (↑toFinsupp a).support ∪ (↑toFinsupp b).support
X : Type u_1
a b : FreeAbelianGroup X
⊢ support (a + b) ⊆ support a ∪ support b
simp only [support, AddMonoidHom.map_add]
no goals
X : Type u_1
a b : FreeAbelianGroup X
⊢ (↑toFinsupp a + ↑toFinsupp b).support ⊆ (↑toFinsupp a).support ∪ (↑toFinsupp b).support
apply Finsupp.support_add