---

Step * of Lemma free-iso-int_wf

∀[S:Type]. ∀[s:S].  free-iso-int(s) ∈ free-vs(ℤ-rng;S) ≅ ℤ supposing ∀x,y:S.  (x = y ∈ S)
BY
{ (Auto THEN (InstLemma `free-1-iso_wf` [⌜S⌝;⌜s⌝;⌜ℤ-rng⌝]⋅ THENA Auto)) }

1
1. S : Type
2. s : S
3. ∀x,y:S.  (x = y ∈ S)
4. free-1-iso(s;ℤ-rng) ∈ free-vs(ℤ-rng;S) ≅ one-dim-vs(ℤ-rng)
⊢ free-iso-int(s) ∈ free-vs(ℤ-rng;S) ≅ ℤ

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[s:S].    free-iso-int(s)  \mmember{}  free-vs(\mBbbZ{}-rng;S)  \mcong{}  \mBbbZ{}  supposing  \mforall{}x,y:S.    (x  =  y)


By

---

Latex:
(Auto  THEN  (InstLemma  `free-1-iso\_wf`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}\mBbbZ{}-rng\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index