Step
*
of Lemma
polyalg_mo_wf
∀S:DSet. ∀A:CRng. ∀p:polynom_alg{i:l}(S;A).  (p.mo ∈ FAbMon(S))
BY
{ ModulePiTac 2 ``polyalg_mo polyalg_poly`` }
Latex:
Latex:
\mforall{}S:DSet.  \mforall{}A:CRng.  \mforall{}p:polynom\_alg\{i:l\}(S;A).    (p.mo  \mmember{}  FAbMon(S))
By
Latex:
ModulePiTac  2  ``polyalg\_mo  polyalg\_poly``
Home
Index