:: On Square-free Numbers
:: by Adam Grabowski
::
:: Received July 12, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


registration
let a, b be non zero Nat;
cluster a gcd b -> non zero ;
coherence
not a gcd b is zero
by INT_2:5;
cluster a lcm b -> non zero ;
coherence
not a lcm b is zero
by INT_2:4;
end;

registration
let n be Nat;
reduce 0 -' n to 0 ;
reducibility
0 -' n = 0
proof end;
end;

theorem :: MOEBIUS2:1
for n, i being Nat st n >= 2 |^ ((2 * i) + 2) holds
n / 2 >= (2 |^ i) * (sqrt n)
proof end;

theorem :: MOEBIUS2:2
for n being Nat holds support (pfexp n) c= SetPrimes
proof end;

theorem FOT1: :: MOEBIUS2:3
for n being non zero Nat holds n - ((n div 2) * 2) <= 1
proof end;

theorem FOTN: :: MOEBIUS2:4
for a, n being non zero Nat holds (n div a) * a <= n
proof end;

theorem RelPrimeEx: :: MOEBIUS2:5
for a, b being non zero Nat st not a,b are_coprime holds
ex k being non zero Nat st
( k <> 1 & k divides a & k divides b )
proof end;

theorem DivNonZero: :: MOEBIUS2:6
for n, a being non zero Nat st a divides n holds
n div a <> 0
proof end;

theorem INT615: :: MOEBIUS2:7
for i, j being Nat st i,j are_coprime holds
i lcm j = i * j
proof end;

registration
let f be natural-valued FinSequence;
cluster Product f -> natural ;
coherence
Product f is natural
proof end;
end;

theorem :: MOEBIUS2:8
primenumber 0 = 2
proof end;

theorem LS2: :: MOEBIUS2:9
SetPrimenumber 3 = {2}
proof end;

theorem :: MOEBIUS2:10
primenumber 1 = 3
proof end;

theorem LS3: :: MOEBIUS2:11
SetPrimenumber 5 = {2,3}
proof end;

theorem :: MOEBIUS2:12
primenumber 2 = 5
proof end;

lem6: 2 divides 2 * 3
;

lem8: 2 divides 2 * 4
;

lem9: 3 divides 3 * 3
;

lem10: 2 divides 2 * 5
;

lem12: 2 divides 2 * 6
;

theorem :: MOEBIUS2:13
SetPrimenumber 6 = {2,3,5}
proof end;

theorem LS4: :: MOEBIUS2:14
SetPrimenumber 7 = {2,3,5}
proof end;

theorem :: MOEBIUS2:15
primenumber 3 = 7
proof end;

theorem LS11: :: MOEBIUS2:16
SetPrimenumber 11 = {2,3,5,7}
proof end;

theorem :: MOEBIUS2:17
primenumber 4 = 11
proof end;

theorem LS13: :: MOEBIUS2:18
SetPrimenumber 13 = {2,3,5,7,11}
proof end;

theorem :: MOEBIUS2:19
primenumber 5 = 13
proof end;

theorem :: MOEBIUS2:20
for m, n being Nat holds
( SetPrimenumber m c= SetPrimenumber n or SetPrimenumber n c= SetPrimenumber m )
proof end;

theorem Cosik1: :: MOEBIUS2:21
for n, m being Nat holds
( n < m iff primenumber n < primenumber m )
proof end;

definition
func ReciPrime -> Real_Sequence means :ReciPr: :: MOEBIUS2:def 1
for i being Nat holds it . i = 1 / (primenumber i);
correctness
existence
ex b1 being Real_Sequence st
for i being Nat holds b1 . i = 1 / (primenumber i)
;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = 1 / (primenumber i) ) & ( for i being Nat holds b2 . i = 1 / (primenumber i) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem ReciPr defines ReciPrime MOEBIUS2:def 1 :
for b1 being Real_Sequence holds
( b1 = ReciPrime iff for i being Nat holds b1 . i = 1 / (primenumber i) );

notation
let f be Real_Sequence;
antonym divergent f for convergent ;
end;

registration
cluster ReciPrime -> decreasing bounded_below ;
coherence
( ReciPrime is decreasing & ReciPrime is bounded_below )
proof end;
end;

registration
cluster ReciPrime -> convergent ;
coherence
not ReciPrime is divergent
;
end;

definition
func invNAT -> Real_Sequence means :DefRec: :: MOEBIUS2:def 2
for i being Nat holds it . i = 1 / i;
correctness
existence
ex b1 being Real_Sequence st
for i being Nat holds b1 . i = 1 / i
;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = 1 / i ) & ( for i being Nat holds b2 . i = 1 / i ) holds
b1 = b2
;
proof end;
end;

:: deftheorem DefRec defines invNAT MOEBIUS2:def 2 :
for b1 being Real_Sequence holds
( b1 = invNAT iff for i being Nat holds b1 . i = 1 / i );

registration
cluster invNAT -> nonnegative-yielding ;
coherence
invNAT is nonnegative-yielding
proof end;
end;

registration
cluster invNAT -> convergent ;
coherence
not invNAT is divergent
proof end;
end;

theorem LimId: :: MOEBIUS2:22
lim invNAT = 0
proof end;

theorem RecSub: :: MOEBIUS2:23
ReciPrime is subsequence of invNAT
proof end;

registration
let f be nonnegative-yielding Real_Sequence;
cluster -> nonnegative-yielding for subsequence of f;
coherence
for b1 being subsequence of f holds b1 is nonnegative-yielding
proof end;
end;

registration
cluster ReciPrime -> nonnegative-yielding ;
coherence
ReciPrime is nonnegative-yielding
by RecSub;
end;

theorem :: MOEBIUS2:24
lim ReciPrime = 0 by LimId, RecSub, SEQ_4:17;

registration
cluster Partial_Sums ReciPrime -> non-decreasing for Real_Sequence;
coherence
for b1 being Real_Sequence st b1 = Partial_Sums ReciPrime holds
b1 is non-decreasing
proof end;
end;

theorem :: MOEBIUS2:25
for f being nonnegative-yielding Real_Sequence st f is summable holds
for p being Real st p > 0 holds
ex i being Element of NAT st Sum (f ^\ i) < p
proof end;

definition
let n be non zero Nat;
func SqFactors n -> ManySortedSet of SetPrimes means :SqDef: :: MOEBIUS2:def 3
( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
it . p = p |^ ((p |-count n) div 2) ) );
existence
ex b1 being ManySortedSet of SetPrimes st
( support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b1 . p = p |^ ((p |-count n) div 2) ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of SetPrimes st support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b1 . p = p |^ ((p |-count n) div 2) ) & support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b2 . p = p |^ ((p |-count n) div 2) ) holds
b1 = b2
proof end;
end;

:: deftheorem SqDef defines SqFactors MOEBIUS2:def 3 :
for n being non zero Nat
for b2 being ManySortedSet of SetPrimes holds
( b2 = SqFactors n iff ( support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b2 . p = p |^ ((p |-count n) div 2) ) ) );

registration
let n be non zero Nat;
cluster SqFactors n -> natural-valued finite-support ;
coherence
( SqFactors n is finite-support & SqFactors n is natural-valued )
proof end;
end;

registration
let n be non zero Nat;
cluster -> natural for Element of support (SqFactors n);
coherence
for b1 being Element of support (SqFactors n) holds b1 is natural
;
end;

definition
let n be non zero Nat;
func SqF n -> Nat equals :: MOEBIUS2:def 4
Product (SqFactors n);
coherence
Product (SqFactors n) is Nat
;
end;

:: deftheorem defines SqF MOEBIUS2:def 4 :
for n being non zero Nat holds SqF n = Product (SqFactors n);

theorem Matsu: :: MOEBIUS2:26
for f being bag of SetPrimes holds Product f <> 0
proof end;

registration
let n be non zero Nat;
cluster SqF n -> non zero ;
coherence
not SqF n is zero
by Matsu;
end;

definition
let p be Prime;
func FreeGen p -> Subset of NAT means :FG: :: MOEBIUS2:def 5
for n being Nat holds
( n in it iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) );
existence
ex b1 being Subset of NAT st
for n being Nat holds
( n in b1 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) )
proof end;
uniqueness
for b1, b2 being Subset of NAT st ( for n being Nat holds
( n in b1 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) ) & ( for n being Nat holds
( n in b2 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem FG defines FreeGen MOEBIUS2:def 5 :
for p being Prime
for b2 being Subset of NAT holds
( b2 = FreeGen p iff for n being Nat holds
( n in b2 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) );

theorem Ex1: :: MOEBIUS2:27
for p being Prime holds 1 in FreeGen p
proof end;

theorem :: MOEBIUS2:28
for p being Prime holds not 0 in FreeGen p by MOEBIUS1:21, FG;

registration
cluster epsilon-transitive epsilon-connected ordinal natural non zero complex V26() ext-real non negative finite cardinal integer dim-like square-free for set ;
existence
ex b1 being Nat st
( b1 is square-free & not b1 is zero )
by MOEBIUS1:22;
end;

registration
let p be Prime;
cluster Relation-like Seg p -defined RAT -valued Function-like V14( Seg p) complex-valued ext-real-valued real-valued natural-valued finite-support positive-yielding for set ;
existence
ex b1 being bag of Seg p st b1 is positive-yielding
proof end;
end;

theorem Thds: :: MOEBIUS2:29
for p being Prime
for f being positive-yielding bag of Seg p holds dom f = support f
proof end;

theorem domcanFS: :: MOEBIUS2:30
for p being Prime holds dom (canFS (Seg p)) = Seg p
proof end;

theorem :: MOEBIUS2:31
for A being finite set holds dom (canFS A) = Seg (card A)
proof end;

theorem ThCon: :: MOEBIUS2:32
for p being Prime
for g being positive-yielding bag of Seg p st g = p |-> p holds
g = g * (canFS (support g))
proof end;

theorem :: MOEBIUS2:33
for p being Prime
for f being positive-yielding bag of Seg p st f = p |-> p holds
Product f = p |^ p
proof end;

theorem Lm1: :: MOEBIUS2:34
for p being Prime
for n being non zero Nat st n in FreeGen p holds
support (pfexp n) c= Seg p
proof end;

theorem :: MOEBIUS2:35
for p being Prime
for n being non zero Nat st n in FreeGen p holds
card (support (pfexp n)) <= p
proof end;

theorem LmRng: :: MOEBIUS2:36
for n being non zero square-free Nat holds rng (pfexp n) c= 2
proof end;

theorem WOW: :: MOEBIUS2:37
for m, n being non zero Nat st pfexp m = pfexp n holds
m = n
proof end;

registration
let p be Prime;
cluster FreeGen p -> non empty ;
coherence
not FreeGen p is empty
by Ex1;
end;

registration
let p be Prime;
cluster -> non empty for Element of FreeGen p;
coherence
for b1 being Element of FreeGen p holds not b1 is empty
by MOEBIUS1:21, FG;
end;

definition
let p be Prime;
func BoolePrime p -> set equals :: MOEBIUS2:def 6
Funcs (((Seg p) /\ SetPrimes),2);
coherence
Funcs (((Seg p) /\ SetPrimes),2) is set
;
end;

:: deftheorem defines BoolePrime MOEBIUS2:def 6 :
for p being Prime holds BoolePrime p = Funcs (((Seg p) /\ SetPrimes),2);

registration
let p be Prime;
cluster BoolePrime p -> finite ;
coherence
BoolePrime p is finite
;
end;

definition
let p be Prime;
func canHom p -> Function of (FreeGen p),(BoolePrime p) means :canH: :: MOEBIUS2:def 7
for x being Element of FreeGen p holds it . x = (pfexp x) | ((Seg p) /\ SetPrimes);
existence
ex b1 being Function of (FreeGen p),(BoolePrime p) st
for x being Element of FreeGen p holds b1 . x = (pfexp x) | ((Seg p) /\ SetPrimes)
proof end;
uniqueness
for b1, b2 being Function of (FreeGen p),(BoolePrime p) st ( for x being Element of FreeGen p holds b1 . x = (pfexp x) | ((Seg p) /\ SetPrimes) ) & ( for x being Element of FreeGen p holds b2 . x = (pfexp x) | ((Seg p) /\ SetPrimes) ) holds
b1 = b2
proof end;
end;

:: deftheorem canH defines canHom MOEBIUS2:def 7 :
for p being Prime
for b2 being Function of (FreeGen p),(BoolePrime p) holds
( b2 = canHom p iff for x being Element of FreeGen p holds b2 . x = (pfexp x) | ((Seg p) /\ SetPrimes) );

registration
let p be Prime;
cluster canHom p -> one-to-one ;
coherence
canHom p is one-to-one
proof end;
end;

theorem FinCar: :: MOEBIUS2:38
for p being Prime holds card (FreeGen p) c= card (BoolePrime p)
proof end;

LmX: for p being Prime holds card (FreeGen p) c= 2 |^ p
proof end;

registration
let p be Prime;
cluster FreeGen p -> finite ;
coherence
FreeGen p is finite
proof end;
end;

theorem :: MOEBIUS2:39
for p being Prime holds card (FreeGen p) <= 2 |^ p
proof end;

theorem Ciek: :: MOEBIUS2:40
for n, i being Nat
for p being Prime st n <> 0 & p |^ i divides n holds
i <= p |-count n
proof end;

theorem MoInv: :: MOEBIUS2:41
for n being Nat st n <> 0 & ( for p being Prime holds p |-count n <= 1 ) holds
n is square-free
proof end;

theorem MB148: :: MOEBIUS2:42
for p being Prime
for n being non zero Nat st p |-count n = 0 holds
(SqFactors n) . p = 0
proof end;

theorem MB149: :: MOEBIUS2:43
for n being non zero Nat
for p being Prime st p |-count n <> 0 holds
(SqFactors n) . p = p |^ ((p |-count n) div 2)
proof end;

theorem MB150: :: MOEBIUS2:44
for m, n being non zero Nat st m,n are_coprime holds
SqFactors (m * n) = (SqFactors m) + (SqFactors n)
proof end;

theorem :: MOEBIUS2:45
for n being non zero Nat holds SqF n divides n
proof end;

registration
let n be non zero Nat;
cluster PFactors n -> prime-factorization-like ;
coherence
PFactors n is prime-factorization-like
proof end;
end;

theorem Matsu0: :: MOEBIUS2:46
for f being bag of SetPrimes ex g being FinSequence of NAT st
( Product f = Product g & g = f * (canFS (support f)) )
proof end;

theorem Matsu1: :: MOEBIUS2:47
for n being Nat
for p being Prime
for f being bag of SetPrimes st f . p = p |^ n holds
p |^ n divides Product f
proof end;

theorem BZE: :: MOEBIUS2:48
for n being Nat
for p being Prime
for f being bag of SetPrimes st f . p = p |^ n holds
p |-count (Product f) >= n
proof end;

definition
let n be non zero Nat;
func TSqFactors n -> ManySortedSet of SetPrimes means :TSqDef: :: MOEBIUS2:def 8
( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
it . p = p |^ (2 * ((p |-count n) div 2)) ) );
existence
ex b1 being ManySortedSet of SetPrimes st
( support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b1 . p = p |^ (2 * ((p |-count n) div 2)) ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of SetPrimes st support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b1 . p = p |^ (2 * ((p |-count n) div 2)) ) & support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b2 . p = p |^ (2 * ((p |-count n) div 2)) ) holds
b1 = b2
proof end;
end;

:: deftheorem TSqDef defines TSqFactors MOEBIUS2:def 8 :
for n being non zero Nat
for b2 being ManySortedSet of SetPrimes holds
( b2 = TSqFactors n iff ( support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b2 . p = p |^ (2 * ((p |-count n) div 2)) ) ) );

theorem :: MOEBIUS2:49
for n being non zero Nat holds TSqFactors n = (SqFactors n) |^ 2
proof end;

registration
let n be non zero Nat;
cluster TSqFactors n -> natural-valued finite-support ;
coherence
( TSqFactors n is finite-support & TSqFactors n is natural-valued )
proof end;
end;

definition
let n be non zero Nat;
func TSqF n -> Nat equals :: MOEBIUS2:def 9
Product (TSqFactors n);
coherence
Product (TSqFactors n) is Nat
;
end;

:: deftheorem defines TSqF MOEBIUS2:def 9 :
for n being non zero Nat holds TSqF n = Product (TSqFactors n);

registration
let n be non zero Nat;
cluster TSqF n -> non zero ;
coherence
not TSqF n is zero
by Matsu;
end;

theorem MB148T: :: MOEBIUS2:50
for p being Prime
for n being non zero Nat st p |-count n = 0 holds
(TSqFactors n) . p = 0
proof end;

theorem MB149T: :: MOEBIUS2:51
for n being non zero Nat
for p being Prime st p |-count n <> 0 holds
(TSqFactors n) . p = p |^ (2 * ((p |-count n) div 2))
proof end;

theorem MB150T: :: MOEBIUS2:52
for m, n being non zero Nat st m,n are_coprime holds
TSqFactors (m * n) = (TSqFactors m) + (TSqFactors n)
proof end;

registration
let n be non zero Nat;
cluster support (TSqFactors n) -> natural-membered ;
coherence
support (TSqFactors n) is natural-membered
;
end;

theorem Skup: :: MOEBIUS2:53
for n being non zero Nat holds TSqF n divides n
proof end;

registration
let n be non zero Nat;
cluster n div (TSqF n) -> square-free for Nat;
coherence
for b1 being Nat st b1 = n div (TSqF n) holds
not b1 is square-containing
proof end;
end;

theorem SqCon1: :: MOEBIUS2:54
for n, k being non zero Nat st k <> 1 & k ^2 divides n holds
n is square-containing
proof end;

theorem DivRelPrime: :: MOEBIUS2:55
for n being non zero square-free Nat
for a being non zero Nat st a divides n holds
a,n div a are_coprime
proof end;

theorem CutComm: :: MOEBIUS2:56
for A, C being non empty set
for L being commutative BinOp of A
for LC being BinOp of C st C c= A & LC = L || C holds
LC is commutative
proof end;

theorem CutAssoc: :: MOEBIUS2:57
for A, C being non empty set
for L being associative BinOp of A
for LC being BinOp of C st C c= A & LC = L || C holds
LC is associative
proof end;

registration
let C be non empty set ;
let L be commutative BinOp of C;
let M be BinOp of C;
cluster LattStr(# C,L,M #) -> join-commutative ;
coherence
LattStr(# C,L,M #) is join-commutative
by BINOP_1:def 2;
end;

registration
let C be non empty set ;
let L be BinOp of C;
let M be commutative BinOp of C;
cluster LattStr(# C,L,M #) -> meet-commutative ;
coherence
LattStr(# C,L,M #) is meet-commutative
by BINOP_1:def 2;
end;

registration
let C be non empty set ;
let L be associative BinOp of C;
let M be BinOp of C;
cluster LattStr(# C,L,M #) -> join-associative ;
coherence
LattStr(# C,L,M #) is join-associative
by BINOP_1:def 3;
end;

registration
let C be non empty set ;
let L be BinOp of C;
let M be associative BinOp of C;
cluster LattStr(# C,L,M #) -> meet-associative ;
coherence
LattStr(# C,L,M #) is meet-associative
by BINOP_1:def 3;
end;

theorem DivInPlus: :: MOEBIUS2:58
for n being non zero Nat holds NatDivisors n c= NATPLUS by NAT_LAT:def 6;

theorem LCMDiv: :: MOEBIUS2:59
for n being non zero Nat
for x, y being Nat st x in NatDivisors n & y in NatDivisors n holds
x lcm y in NatDivisors n
proof end;

theorem GCDDiv: :: MOEBIUS2:60
for n being non zero Nat
for x, y being Nat st x in NatDivisors n & y in NatDivisors n holds
x gcd y in NatDivisors n
proof end;

registration
let n be non zero Nat;
cluster NatDivisors n -> non empty ;
coherence
not NatDivisors n is empty
by MOEBIUS1:39;
end;

registration
cluster hcflat -> commutative associative ;
coherence
( hcflat is commutative & hcflat is associative )
by NAT_LAT:def 3;
cluster lcmlat -> commutative associative ;
coherence
( lcmlat is commutative & lcmlat is associative )
by NAT_LAT:def 3;
end;

theorem HcfLat: :: MOEBIUS2:61
hcflatplus = hcflat || NATPLUS
proof end;

theorem LcmLat: :: MOEBIUS2:62
lcmlatplus = lcmlat || NATPLUS
proof end;

registration
cluster hcflatplus -> commutative ;
coherence
hcflatplus is commutative
by CutComm, HcfLat;
cluster lcmlatplus -> commutative ;
coherence
lcmlatplus is commutative
by CutComm, LcmLat;
cluster hcflatplus -> associative ;
coherence
hcflatplus is associative
by CutAssoc, HcfLat;
cluster lcmlatplus -> associative ;
coherence
lcmlatplus is associative
by CutAssoc, LcmLat;
end;

:: WP: The lattice of natural divisors
definition
let n be non zero Nat;
func Divisors_Lattice n -> strict SubLattice of NatPlus_Lattice means :DivLat: :: MOEBIUS2:def 10
the carrier of it = NatDivisors n;
existence
ex b1 being strict SubLattice of NatPlus_Lattice st the carrier of b1 = NatDivisors n
proof end;
uniqueness
for b1, b2 being strict SubLattice of NatPlus_Lattice st the carrier of b1 = NatDivisors n & the carrier of b2 = NatDivisors n holds
b1 = b2
proof end;
end;

:: deftheorem DivLat defines Divisors_Lattice MOEBIUS2:def 10 :
for n being non zero Nat
for b2 being strict SubLattice of NatPlus_Lattice holds
( b2 = Divisors_Lattice n iff the carrier of b2 = NatDivisors n );

registration
let n be non zero Nat;
cluster the carrier of (Divisors_Lattice n) -> natural-membered ;
coherence
the carrier of (Divisors_Lattice n) is natural-membered
proof end;
end;

theorem OperLat: :: MOEBIUS2:63
for n being non zero Nat
for a, b being Element of (Divisors_Lattice n) holds
( a "\/" b = a lcm b & a "/\" b = a gcd b )
proof end;

registration
let n be non zero Nat;
let p, q be Element of (Divisors_Lattice n);
identify p "\/" q with p lcm q;
correctness
compatibility
p "\/" q = p lcm q
;
by OperLat;
identify p "/\" q with p gcd q;
correctness
compatibility
p "/\" q = p gcd q
;
by OperLat;
end;

registration
let n be non zero Nat;
cluster Divisors_Lattice n -> non empty strict ;
coherence
not Divisors_Lattice n is empty
;
end;

registration
let n be non zero Nat;
cluster Divisors_Lattice n -> strict distributive bounded ;
coherence
( Divisors_Lattice n is distributive & Divisors_Lattice n is bounded )
proof end;
end;

theorem TopBot: :: MOEBIUS2:64
for n being non zero Nat holds
( Top (Divisors_Lattice n) = n & Bottom (Divisors_Lattice n) = 1 )
proof end;

SquareBool0: for n being non zero square-free Nat holds Divisors_Lattice n is Boolean
proof end;

registration
let n be non zero square-free Nat;
cluster Divisors_Lattice n -> strict Boolean ;
coherence
Divisors_Lattice n is Boolean
by SquareBool0;
end;

registration
let n be non zero Nat;
cluster -> non zero for Element of the carrier of (Divisors_Lattice n);
coherence
for b1 being Element of (Divisors_Lattice n) holds not b1 is zero
proof end;
end;

theorem :: MOEBIUS2:65
for n being non zero Nat holds
( Divisors_Lattice n is Boolean iff n is square-free )
proof end;