Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
have split off tensor product of abelian groups from tensor product and expanded slightly
added to tensor product of abelian groups the examples $A \otimes \mathbb{Z} \simeq A$ and $\mathbb{Z}_a \otimes \mathbb{Z}_b \simeq \mathbb{Z}_{LCM(a,b)}$.
In the Definition-section I have made the quotient map $A \times B \to A \otimes B$ more explicit.
added definition of the tensor product of abelian groups as a quotient inductive type
Anonymous
1 to 9 of 9