Step * of Lemma mul_mon_of_rng_wf_c

[r:Rng]. (r↓xmn ∈ IMonoid)
BY
Unfold `mul_mon_of_rng` 
THEN ((D 0) THENA Auto) }

1
1. Rng
⊢ <|r|, =b, ≤b*, 1, λz.z> ∈ IMonoid


Latex:


Latex:
\mforall{}[r:Rng].  (r\mdownarrow{}xmn  \mmember{}  IMonoid)


By


Latex:
Unfold  `mul\_mon\_of\_rng`  0 
THEN  ((D  0)  THENA  Auto)




Home Index