Global Index

E

F

J

K

T

W

X

Y

_

other

(99 entries)

Variable Index

A

B

C

D

E

F

H

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(20 entries)

Library Index

A

B

C

D

E

F

H

I

J

K

N

O

P

Q

S

T

U

V

W

X

Y

_

other

(6 entries)

Lemma Index

E

F

H

J

K

L

Q

T

V

W

X

Y

_

other

(42 entries)

Constructor Index

A

C

D

E

F

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Inductive Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

S

T

U

W

X

Y

Z

_

other

(2 entries)

Section Index

A

B

C

D

E

F

H

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Definition Index

B

E

F

J

K

L

M

R

S

T

U

V

W

X

Y

Z

_

other

(23 entries)

Global Index

A

acc_Q [lemma, in ZChinese.Zgcd]
acc_P [lemma, in ZChinese.Zgcd]
add_add [lemma, in ZChinese.groups]
antisym [definition, in ZChinese.misc]
associativity [definition, in ZChinese.Lci]

B

Bezout_exists [lemma, in ZChinese.Zgcd]
Bezout_i [constructor, in ZChinese.Zgcd]

C

chinese_remaindering_theorem [lemma, in ZChinese.Zgcd]
commutativity [definition, in ZChinese.Lci]
congruentZ [definition, in ZChinese.Zgcd]

D

distributivity [definition, in ZChinese.Lci]
divide [definition, in ZChinese.rings]
divide_selfZ [lemma, in ZChinese.Zgcd]
div_opp [lemma, in ZChinese.rings]
div_mult [lemma, in ZChinese.rings]
div_add [lemma, in ZChinese.rings]
div_O_O [lemma, in ZChinese.rings]

G

gcdZ [definition, in ZChinese.Zgcd]
gcdZ_is_gcdZ [lemma, in ZChinese.Zgcd]
gcdZ_correct [lemma, in ZChinese.Zgcd]
gcdZ_is_gcd [lemma, in ZChinese.Zgcd]
gcdZ_exists [lemma, in ZChinese.Zgcd]
gcdZ_i [definition, in ZChinese.Zgcd]
gcd_unicity_apart_unities [lemma, in ZChinese.rings]
gcd_null2 [lemma, in ZChinese.rings]
gcd_null [lemma, in ZChinese.rings]
gcd_modZ [lemma, in ZChinese.Zgcd]
gcd_mod [constructor, in ZChinese.Zgcd]
gcd_OZ [constructor, in ZChinese.Zgcd]
gcd_OZ_absZ [lemma, in ZChinese.Zgcd]
gcd_unicity_apart_sign [lemma, in ZChinese.Zgcd]
groups [section, in ZChinese.groups]
groups [library]
groups.Add [variable, in ZChinese.groups]
groups.G [variable, in ZChinese.groups]
groups.O [variable, in ZChinese.groups]
groups.Opp [variable, in ZChinese.groups]
groups.S [variable, in ZChinese.groups]

H

have_gcdZ [definition, in ZChinese.Zgcd]

I

IdZ [definition, in ZChinese.Zstruct]
integrity [definition, in ZChinese.rings]
integrityZ [lemma, in ZChinese.Zstruct]
intern [definition, in ZChinese.Lci]
Internal [section, in ZChinese.Lci]
Internal.Add [variable, in ZChinese.Lci]
Internal.G [variable, in ZChinese.Lci]
Internal.I [variable, in ZChinese.Lci]
Internal.Inv [variable, in ZChinese.Lci]
Internal.O [variable, in ZChinese.Lci]
Internal.Opp [variable, in ZChinese.Lci]
Internal.S [variable, in ZChinese.Lci]
inversible [definition, in ZChinese.misc]
inversibleZ [lemma, in ZChinese.Zstruct]
inv_com [lemma, in ZChinese.misc]
is_opposite [definition, in ZChinese.Lci]
is_gcd [definition, in ZChinese.rings]
is_unitary_commutative_ring [definition, in ZChinese.rings]
is_ring [definition, in ZChinese.rings]
is_gcdZ [inductive, in ZChinese.Zgcd]
is_group [definition, in ZChinese.groups]

L

Lci [library]

M

misc [library]
mult_opp_opp [lemma, in ZChinese.rings]
mult_opp_l [lemma, in ZChinese.rings]
mult_opp_r [lemma, in ZChinese.rings]
mult_O [lemma, in ZChinese.rings]

N

neutral [definition, in ZChinese.Lci]
neutral_add [lemma, in ZChinese.Lci]

O

opposite [definition, in ZChinese.Lci]
opp_com [lemma, in ZChinese.Lci]
opp_O [lemma, in ZChinese.rings]
opp_neutral [lemma, in ZChinese.groups]
opp_add [lemma, in ZChinese.groups]
opp_opp [lemma, in ZChinese.groups]
opp_unicity [lemma, in ZChinese.groups]

P

P [definition, in ZChinese.Zgcd]
pi1 [definition, in ZChinese.misc]
pi2 [lemma, in ZChinese.misc]
positive_is_gcdZ [lemma, in ZChinese.Zgcd]

Q

Q [definition, in ZChinese.Zgcd]

R

regular_l [lemma, in ZChinese.groups]
ring [section, in ZChinese.rings]
rings [library]
ring.A [variable, in ZChinese.rings]
ring.Add [variable, in ZChinese.rings]
ring.I [variable, in ZChinese.rings]
ring.Mult [variable, in ZChinese.rings]
ring.O [variable, in ZChinese.rings]
ring.Opp [variable, in ZChinese.rings]
ring.S [variable, in ZChinese.rings]
ring.v [variable, in ZChinese.rings]

S

simplification_integrity [lemma, in ZChinese.rings]

U

unicity_is_gcdZ [lemma, in ZChinese.Zgcd]

V

verify_BezoutZ [inductive, in ZChinese.Zgcd]

Z

Zgcd [library]
Zstruct [library]
Z_unitary_commutative_ring [lemma, in ZChinese.Zstruct]
Z_ring [lemma, in ZChinese.Zstruct]
Z_group [lemma, in ZChinese.Zstruct]

Variable Index

G

groups.Add [in ZChinese.groups]
groups.G [in ZChinese.groups]
groups.O [in ZChinese.groups]
groups.Opp [in ZChinese.groups]
groups.S [in ZChinese.groups]

I

Internal.Add [in ZChinese.Lci]
Internal.G [in ZChinese.Lci]
Internal.I [in ZChinese.Lci]
Internal.Inv [in ZChinese.Lci]
Internal.O [in ZChinese.Lci]
Internal.Opp [in ZChinese.Lci]
Internal.S [in ZChinese.Lci]

R

ring.A [in ZChinese.rings]
ring.Add [in ZChinese.rings]
ring.I [in ZChinese.rings]
ring.Mult [in ZChinese.rings]
ring.O [in ZChinese.rings]
ring.Opp [in ZChinese.rings]
ring.S [in ZChinese.rings]
ring.v [in ZChinese.rings]

Library Index

G

groups

L

Lci

M

misc

R

rings

Z

Lemma Index

A

acc_Q [in ZChinese.Zgcd]
acc_P [in ZChinese.Zgcd]
add_add [in ZChinese.groups]

B

Bezout_exists [in ZChinese.Zgcd]

C

chinese_remaindering_theorem [in ZChinese.Zgcd]

D

divide_selfZ [in ZChinese.Zgcd]
div_opp [in ZChinese.rings]
div_mult [in ZChinese.rings]
div_add [in ZChinese.rings]
div_O_O [in ZChinese.rings]

G

gcdZ_is_gcdZ [in ZChinese.Zgcd]
gcdZ_correct [in ZChinese.Zgcd]
gcdZ_is_gcd [in ZChinese.Zgcd]
gcdZ_exists [in ZChinese.Zgcd]
gcd_unicity_apart_unities [in ZChinese.rings]
gcd_null2 [in ZChinese.rings]
gcd_null [in ZChinese.rings]
gcd_modZ [in ZChinese.Zgcd]
gcd_OZ_absZ [in ZChinese.Zgcd]
gcd_unicity_apart_sign [in ZChinese.Zgcd]

I

integrityZ [in ZChinese.Zstruct]
inversibleZ [in ZChinese.Zstruct]
inv_com [in ZChinese.misc]

M

mult_opp_opp [in ZChinese.rings]
mult_opp_l [in ZChinese.rings]
mult_opp_r [in ZChinese.rings]
mult_O [in ZChinese.rings]

N

neutral_add [in ZChinese.Lci]

O

opp_com [in ZChinese.Lci]
opp_O [in ZChinese.rings]
opp_neutral [in ZChinese.groups]
opp_add [in ZChinese.groups]
opp_opp [in ZChinese.groups]
opp_unicity [in ZChinese.groups]

P

pi2 [in ZChinese.misc]
positive_is_gcdZ [in ZChinese.Zgcd]

R

regular_l [in ZChinese.groups]

S

simplification_integrity [in ZChinese.rings]

U

unicity_is_gcdZ [in ZChinese.Zgcd]

Z

Z_unitary_commutative_ring [in ZChinese.Zstruct]
Z_ring [in ZChinese.Zstruct]
Z_group [in ZChinese.Zstruct]

Constructor Index

B

Bezout_i [in ZChinese.Zgcd]

G

gcd_mod [in ZChinese.Zgcd]
gcd_OZ [in ZChinese.Zgcd]

Inductive Index

I

is_gcdZ [in ZChinese.Zgcd]

V

verify_BezoutZ [in ZChinese.Zgcd]

Section Index

G

groups [in ZChinese.groups]

I

Internal [in ZChinese.Lci]

R

ring [in ZChinese.rings]

Definition Index

A

antisym [in ZChinese.misc]
associativity [in ZChinese.Lci]

C

commutativity [in ZChinese.Lci]
congruentZ [in ZChinese.Zgcd]

D

distributivity [in ZChinese.Lci]
divide [in ZChinese.rings]

G

gcdZ [in ZChinese.Zgcd]
gcdZ_i [in ZChinese.Zgcd]

H

have_gcdZ [in ZChinese.Zgcd]

I

IdZ [in ZChinese.Zstruct]
integrity [in ZChinese.rings]
intern [in ZChinese.Lci]
inversible [in ZChinese.misc]
is_opposite [in ZChinese.Lci]
is_gcd [in ZChinese.rings]
is_unitary_commutative_ring [in ZChinese.rings]
is_ring [in ZChinese.rings]
is_group [in ZChinese.groups]

N

neutral [in ZChinese.Lci]

O

opposite [in ZChinese.Lci]

P

P [in ZChinese.Zgcd]
pi1 [in ZChinese.misc]

Q

Q [in ZChinese.Zgcd]

Global Index

E

F

J

K

T

W

X

Y

_

other

(99 entries)

Variable Index

A

B

C

D

E

F

H

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(20 entries)

Library Index

A

B

C

D

E

F

H

I

J

K

N

O

P

Q

S

T

U

V

W

X

Y

_

other

(6 entries)

Lemma Index

E

F

H

J

K

L

Q

T

V

W

X

Y

_

other

(42 entries)

Constructor Index

A

C

D

E

F

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Inductive Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

S

T

U

W

X

Y

Z

_

other

(2 entries)

Section Index

A

B

C

D

E

F

H

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Definition Index

B

E

F

J

K

L

M

R

S

T

U

V

W

X

Y

Z

_

other

(23 entries)