:: Free Modules
:: by Michal Muzalewski
::
:: Received October 18, 1991
:: Copyright (c) 1991 Association of Mizar Users
Lm1:
for R being Ring
for a being Scalar of R st - a = 0. R holds
a = 0. R
theorem :: MOD_3:1
canceled;
theorem Th2: :: MOD_3:2
theorem :: MOD_3:3
canceled;
theorem :: MOD_3:4
canceled;
theorem :: MOD_3:5
canceled;
theorem Th6: :: MOD_3:6
theorem Th7: :: MOD_3:7
:: deftheorem Def1 defines Lin MOD_3:def 1 :
theorem :: MOD_3:8
canceled;
theorem :: MOD_3:9
canceled;
theorem :: MOD_3:10
canceled;
theorem Th11: :: MOD_3:11
theorem Th12: :: MOD_3:12
theorem Th13: :: MOD_3:13
theorem :: MOD_3:14
theorem Th15: :: MOD_3:15
theorem :: MOD_3:16
theorem Th17: :: MOD_3:17
theorem :: MOD_3:18
theorem :: MOD_3:19
theorem :: MOD_3:20
:: deftheorem Def2 defines base MOD_3:def 2 :
:: deftheorem Def3 defines free MOD_3:def 3 :
theorem Th21: :: MOD_3:21
Lm2:
for R being Skew-Field
for a being Scalar of R
for V being LeftMod of R
for v being Vector of V st a <> 0. R holds
( (a " ) * (a * v) = (1. R) * v & ((a " ) * a) * v = (1. R) * v )
theorem :: MOD_3:22
canceled;
theorem :: MOD_3:23
theorem Th24: :: MOD_3:24
theorem :: MOD_3:25
theorem Th26: :: MOD_3:26
theorem Th27: :: MOD_3:27
Lm3:
for R being Skew-Field
for V being LeftMod of R ex B being Subset of V st B is base
theorem :: MOD_3:28
:: deftheorem MOD_3:def 4 :
canceled;
:: deftheorem Def5 defines Basis MOD_3:def 5 :
theorem :: MOD_3:29
theorem :: MOD_3:30