Step * of Lemma rng_one_wf

[r:RngSig]. (1 ∈ |r|)
BY
ModulePiTac ``rng_car rng_eq rng_le rng_plus rng_zero rng_minus rng_times rng_one rng_div`` }


Latex:


Latex:
\mforall{}[r:RngSig].  (1  \mmember{}  |r|)


By


Latex:
ModulePiTac  9  ``rng\_car  rng\_eq  rng\_le  rng\_plus  rng\_zero  rng\_minus  rng\_times  rng\_one  rng\_div``




Home Index