Solution (source code)

= Solution

In a <coordinate chart>, define the <exterior derivative> by
$$
d\left(\sum_Ia_I\,dx^{i_1}\wedge\cdots\wedge dx^{i_r}\right)
=\sum_Ida_I\wedge dx^{i_1}\wedge\cdots\wedge dx^{i_r}.
$$
The chain rule makes this independent of coordinates. It is real linear, increases form degree by one, agrees with the differential on functions, satisfies $d^2=0$, and obeys the <graded Leibniz rule>
$$
d(\alpha\wedge\beta)=d\alpha\wedge\beta+(-1)^r\alpha\wedge d\beta.
$$
It also commutes with <pullback> by a <smooth map>. These properties characterize it locally and hence globally.

<de Rham cohomology> is the quotient of closed forms by exact forms. If $d\alpha=d\beta=0$, Leibniz gives $d(\alpha\wedge\beta)=0$. Changing $\alpha$ to $\alpha+d\eta$ changes the product by $d(\eta\wedge\beta)$; changing $\beta$ to $\beta+d\xi$ changes it by $(-1)^rd(\alpha\wedge\xi)$. Thus
$$
\boxed{[\alpha][\beta]=[\alpha\wedge\beta]}
$$
is independent of representatives. This gives the graded-commutative <de Rham cohomology> ring.