@MISC{MOEBIUS1.MIZ,
  AUTHOR = {Jastrz\c{e}bska, Magdalena and Grabowski, Adam},
  TITLE = {On the Properties of the {M}\"obius Function},
  SECTION1 = {Preliminaries},
  SECTION2 = {Squarefree Numbers},
  SECTION3 = {M\"obius Function},
  SECTION4 = {Natural Divisors},
  SECTION5 = {The Sum of Values of M\"obius Function},
  SECTION6 = {Prime Factors of a Number},
  SECTION7 = {The Radical of a Number},
  DAY = {21},
  MONTH = {March},
  YEAR = {2006},
  ADDRESS1 = {Institute of Mathematics\\University of Bia{\l}ystok\\Akademicka 2, 15-267 Bia{\l}ystok, Poland},
  ADDRESS2 = {Institute of Mathematics\\University of Bia{\l}ystok\\Akademicka 2, 15-267 Bia{\l}ystok, Poland},
  SUMMARY = {We formalized some basic properties of the M\"obius function which is 
  defined classically as
  \par
  $\mu(n)
  = \left\{\begin{array}{l}
  1,
  \HM{ if }
  n = 1, \\
  \par
  0,
  \HM{ if }
  p^2|n \textrm{~for~some~prime~}p, \\
  \par
  (-1)^r,
  \HM{ if }
  n=p_1 p_2 \cdots p_r, \textrm{~where~} p_i   \textrm{~are~distinct~primes}.
  \end{array}\right.
  $
  \par
  as e.g.,
  its multiplicativity. To enable smooth reasoning about the sum of this
  number-theoretic function, we introduced an underlying many-sorted set
  indexed by the set of natural numbers. Its elements are just values of
  the M\"obius function.\par
  The second part of the paper is devoted to the notion of
  the radical of number, i.e. the product of its all prime factors.\par
  The formalization (which is very much like the one developed in Isabelle
  proof assistant connected with Avigad's formal proof of Prime Number
  Theorem) was done according to the book \cite{HardyWright}.}}

