:: On the Properties of the {M}\"obius Function
:: by Magdalena Jastrz\c{e}bska and Adam Grabowski
::
:: Received March 21, 2006
:: Copyright (c) 2006 Association of Mizar Users
Lm1:
for X, Y, Z, x being set st X misses Y & x in X /\ Z holds
not x in Y /\ Z
theorem Th1: :: MOEBIUS1:1
theorem :: MOEBIUS1:2
theorem :: MOEBIUS1:3
Lm2:
for n being natural number st n <> 1 holds
ex p being Prime st p divides n
theorem Th4: :: MOEBIUS1:4
theorem Th5: :: MOEBIUS1:5
theorem Th6: :: MOEBIUS1:6
theorem Th7: :: MOEBIUS1:7
theorem Th8: :: MOEBIUS1:8
theorem Th9: :: MOEBIUS1:9
theorem Th10: :: MOEBIUS1:10
theorem Th11: :: MOEBIUS1:11
theorem Th12: :: MOEBIUS1:12
theorem :: MOEBIUS1:13
theorem Th14: :: MOEBIUS1:14
theorem Th15: :: MOEBIUS1:15
theorem Th16: :: MOEBIUS1:16
theorem Th17: :: MOEBIUS1:17
theorem Th18: :: MOEBIUS1:18
theorem Th19: :: MOEBIUS1:19
:: deftheorem Def1 defines square-containing MOEBIUS1:def 1 :
theorem Th20: :: MOEBIUS1:20
theorem Th21: :: MOEBIUS1:21
theorem Th22: :: MOEBIUS1:22
theorem Th23: :: MOEBIUS1:23
:: deftheorem Def2 defines SCNAT MOEBIUS1:def 2 :
theorem Th24: :: MOEBIUS1:24
theorem Th25: :: MOEBIUS1:25
theorem Th26: :: MOEBIUS1:26
theorem Th27: :: MOEBIUS1:27
theorem Th28: :: MOEBIUS1:28
theorem :: MOEBIUS1:29
:: deftheorem Def3 defines Moebius MOEBIUS1:def 3 :
theorem Th30: :: MOEBIUS1:30
theorem :: MOEBIUS1:31
theorem :: MOEBIUS1:32
theorem Th33: :: MOEBIUS1:33
theorem Th34: :: MOEBIUS1:34
theorem Th35: :: MOEBIUS1:35
theorem :: MOEBIUS1:36
theorem :: MOEBIUS1:37
theorem Th38: :: MOEBIUS1:38
:: deftheorem defines NatDivisors MOEBIUS1:def 4 :
theorem :: MOEBIUS1:39
theorem Th40: :: MOEBIUS1:40
theorem Th41: :: MOEBIUS1:41
:: deftheorem Def5 defines SMoebius MOEBIUS1:def 5 :
theorem :: MOEBIUS1:42
theorem :: MOEBIUS1:43
theorem :: MOEBIUS1:44
:: deftheorem Def6 defines PFactors MOEBIUS1:def 6 :
theorem Th45: :: MOEBIUS1:45
theorem Th46: :: MOEBIUS1:46
theorem Th47: :: MOEBIUS1:47
theorem Th48: :: MOEBIUS1:48
theorem Th49: :: MOEBIUS1:49
theorem Th50: :: MOEBIUS1:50
theorem :: MOEBIUS1:51
:: deftheorem defines Radical MOEBIUS1:def 7 :
theorem Th52: :: MOEBIUS1:52
theorem :: MOEBIUS1:53
theorem Th54: :: MOEBIUS1:54
theorem Th55: :: MOEBIUS1:55
theorem Th56: :: MOEBIUS1:56
theorem Th57: :: MOEBIUS1:57
theorem :: MOEBIUS1:58
theorem :: MOEBIUS1:59
theorem :: MOEBIUS1:60
theorem Th61: :: MOEBIUS1:61
Lm3:
for n being non zero natural number
for p being Prime holds not p |^ 2 divides Radical n
Lm4:
for n being non zero natural number holds not Radical n is square-containing
theorem :: MOEBIUS1:62
theorem :: MOEBIUS1:63
theorem :: MOEBIUS1:64
Lm5:
for m, n being non zero Element of NAT st m divides n & not m is square-containing holds
m divides Radical n
theorem Th65: :: MOEBIUS1:65
theorem :: MOEBIUS1:66