:: 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 b₁ being Real_Sequence st
for i being Nat holds b₁ . i = 1 / (primenumber i);
uniqueness
for b₁, b₂ being Real_Sequence st ( for i being Nat holds b₁ . i = 1 / (primenumber i) ) & ( for i being Nat holds b₂ . i = 1 / (primenumber i) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem ReciPr defines ReciPrime MOEBIUS2:def 1 :
for b₁ being Real_Sequence holds
( b₁ = ReciPrime iff for i being Nat holds b₁ . 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 b₁ being Real_Sequence st
for i being Nat holds b₁ . i = 1 / i;
uniqueness
for b₁, b₂ being Real_Sequence st ( for i being Nat holds b₁ . i = 1 / i ) & ( for i being Nat holds b₂ . i = 1 / i ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem DefRec defines invNAT MOEBIUS2:def 2 :
for b₁ being Real_Sequence holds
( b₁ = invNAT iff for i being Nat holds b₁ . 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 b₁ being subsequence of f holds b₁ 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 b₁ being Real_Sequence st b₁ = Partial_Sums ReciPrime holds
b₁ 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 b₁ being ManySortedSet of SetPrimes st
( support b₁ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₁ . p = p |^ ((p |-count n) div 2) ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of SetPrimes st support b₁ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₁ . p = p |^ ((p |-count n) div 2) ) & support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . p = p |^ ((p |-count n) div 2) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem SqDef defines SqFactors MOEBIUS2:def 3 :
for n being non zero Nat
for b₂ being ManySortedSet of SetPrimes holds
( b₂ = SqFactors n iff ( support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . 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 b₁ being Element of support (SqFactors n) holds b₁ 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 b₁ being Subset of NAT st
for n being Nat holds
( n in b₁ iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) )

proof end;

uniqueness
for b₁, b₂ being Subset of NAT st ( for n being Nat holds
( n in b₁ iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) ) & ( for n being Nat holds
( n in b₂ iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem FG defines FreeGen MOEBIUS2:def 5 :
for p being Prime
for b₂ being Subset of NAT holds
( b₂ = FreeGen p iff for n being Nat holds
( n in b₂ 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 b₁ being Nat st
( b₁ is square-free & not b₁ 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 b₁ being bag of Seg p st b₁ 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 b₁ being Element of FreeGen p holds not b₁ 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 b₁ being Function of (FreeGen p),(BoolePrime p) st
for x being Element of FreeGen p holds b₁ . x = (pfexp x) | ((Seg p) /\ SetPrimes)

proof end;

uniqueness
for b₁, b₂ being Function of (FreeGen p),(BoolePrime p) st ( for x being Element of FreeGen p holds b₁ . x = (pfexp x) | ((Seg p) /\ SetPrimes) ) & ( for x being Element of FreeGen p holds b₂ . x = (pfexp x) | ((Seg p) /\ SetPrimes) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem canH defines canHom MOEBIUS2:def 7 :
for p being Prime
for b₂ being Function of (FreeGen p),(BoolePrime p) holds
( b₂ = canHom p iff for x being Element of FreeGen p holds b₂ . 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 b₁ being ManySortedSet of SetPrimes st
( support b₁ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₁ . p = p |^ (2 * ((p |-count n) div 2)) ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of SetPrimes st support b₁ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₁ . p = p |^ (2 * ((p |-count n) div 2)) ) & support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . p = p |^ (2 * ((p |-count n) div 2)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem TSqDef defines TSqFactors MOEBIUS2:def 8 :
for n being non zero Nat
for b₂ being ManySortedSet of SetPrimes holds
( b₂ = TSqFactors n iff ( support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . 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 b₁ being Nat st b₁ = n div (TSqF n) holds
not b₁ 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;

:: 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 b₁ being strict SubLattice of NatPlus_Lattice st the carrier of b₁ = NatDivisors n

proof end;

uniqueness
for b₁, b₂ being strict SubLattice of NatPlus_Lattice st the carrier of b₁ = NatDivisors n & the carrier of b₂ = NatDivisors n holds
b₁ = b₂

proof end;

end;

:: deftheorem DivLat defines Divisors_Lattice MOEBIUS2:def 10 :
for n being non zero Nat
for b₂ being strict SubLattice of NatPlus_Lattice holds
( b₂ = Divisors_Lattice n iff the carrier of b₂ = 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 b₁ being Element of (Divisors_Lattice n) holds not b₁ 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;