English
In FreeCommRing, the product corresponding to a ::ₘ m equals the product of the image of a and the image of m in FreeCommRing.
Русский
В FreeCommRing произведение, соответствующее a ::ₘ m, равно произведению образа a и образа m в FreeCommRing.
LaTeX
$$$ \\mathrm{FreeAbelianGroup.of}(\\mathrm{Multiplicative.ofAdd}(a ::_m m)) = \\mathrm{HMul}(\\mathrm{FreeCommRing.of}(a), \\mathrm{FreeAbelianGroup.of}(\\mathrm{Multiplicative.ofAdd}(m))) $$$
Lean4
theorem of_cons (a : α) (m : Multiset α) :
(FreeAbelianGroup.of (Multiplicative.ofAdd (a ::ₘ m))) =
@HMul.hMul _ (FreeCommRing α) (FreeCommRing α) _ (of a) (FreeAbelianGroup.of (Multiplicative.ofAdd m)) :=
by
dsimp [FreeCommRing]
rw [← Multiset.singleton_add, ofAdd_add, of, FreeAbelianGroup.of_mul_of]
