Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(5434 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(89 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(58 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(2752 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(233 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(145 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(139 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(50 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1267 entries)

Moduleid Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(47 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(24 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(609 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(21 entries)

---

G

gauss [lemma, in polydiv]
gauss [lemma, in div]
gauss_gcdl [lemma, in div]
gauss_gcdr [lemma, in div]
gauss_inv [lemma, in div]
gcdn [definition, in div]
gcdnA [lemma, in div]
gcdnAC [lemma, in div]
gcdnC [lemma, in div]
gcdnCA [lemma, in div]
gcdnE [lemma, in div]
gcdnn [lemma, in div]
gcdn0 [lemma, in div]
gcdn1 [lemma, in div]
gcdn_addl [lemma, in div]
gcdn_addl_mul [lemma, in div]
gcdn_addoid [definition, in bigops]
gcdn_addr [lemma, in div]
gcdn_comoid [definition, in bigops]
gcdn_def [lemma, in div]
gcdn_divnC [lemma, in div]
gcdn_gt0 [lemma, in div]
gcdn_modl [lemma, in div]
gcdn_modr [lemma, in div]
gcdn_monoid [definition, in bigops]
gcdn_mull [lemma, in div]
gcdn_mulr [lemma, in div]
gcdn_mul2l [lemma, in div]
gcdn_rec [definition, in div]
gcdp [definition, in poly]
gcdpC [lemma, in poly]
gcdpE [lemma, in poly]
gcdpp [lemma, in poly]
gcdpT [definition, in closedfields]
gcdpTP [lemma, in closedfields]
gcdpTs [definition, in closedfields]
gcdpTsP [lemma, in closedfields]
gcdpTs_qf [lemma, in closedfields]
gcdpT_qf [lemma, in closedfields]
gcdp0 [lemma, in poly]
gcdp_eqp1 [lemma, in polydiv]
gcdp_eq0 [lemma, in polydiv]
gcdp_loop [definition, in closedfields]
gcdp_loopP [lemma, in closedfields]
gcdp_loopT [definition, in closedfields]
gcdp_loopT_qf [lemma, in closedfields]
gcdp_map [lemma, in poly]
gcd0n [lemma, in div]
gcd0p [lemma, in poly]
gcd1n [lemma, in div]
gcd1p [lemma, in polydiv]
gdcop [definition, in polydiv]
gdcopP [lemma, in polydiv]
GdcopSpec [constructor, in polydiv]
gdcopT [definition, in closedfields]
gdcopTP [lemma, in closedfields]
gdcopT_qf [lemma, in closedfields]
gdcop0 [lemma, in polydiv]
gdcop_rec [definition, in polydiv]
gdcop_recP [lemma, in polydiv]
gdcop_recT [definition, in closedfields]
gdcop_recTP [lemma, in closedfields]
gdcop_recT_qf [lemma, in closedfields]
gdcop_spec [inductive, in polydiv]
geq [definition, in ssrnat]
GeqNotLtn [constructor, in ssrnat]
geq_leqif [lemma, in ssrnat]
GRing [moduleid, in ssralg]
GRing.Add [constructor, in ssralg]
GRing.add [definition, in ssralg]
GRing.addIr [lemma, in ssralg]
GRing.addKr [lemma, in ssralg]
GRing.addNKr [lemma, in ssralg]
GRing.addNr [lemma, in ssralg]
GRing.addoid [definition, in ssralg]
GRing.addrA [lemma, in ssralg]
GRing.addrAC [lemma, in ssralg]
GRing.addrC [lemma, in ssralg]
GRing.addrCA [lemma, in ssralg]
GRing.addrI [lemma, in ssralg]
GRing.addrK [lemma, in ssralg]
GRing.addrN [lemma, in ssralg]
GRing.addrNK [lemma, in ssralg]
GRing.addr0 [lemma, in ssralg]
GRing.add0r [lemma, in ssralg]
GRing.add_comoid [definition, in ssralg]
GRing.add_monoid [definition, in ssralg]
GRing.AlgebraTheory [section, in ssralg]
GRing.AlgebraTheory.A [variable, in ssralg]
GRing.AlgebraTheory.R [variable, in ssralg]
GRing.Algebra.Algebra [section, in ssralg]
GRing.Algebra.Algebra.R [variable, in ssralg]
GRing.Algebra.axiom [definition, in ssralg]
GRing.Algebra.base [projection, in ssralg]
GRing.Algebra.choiceType [definition, in ssralg]
GRing.Algebra.class [definition, in ssralg]
GRing.Algebra.Class [constructor, in ssralg]
GRing.Algebra.class_of [record, in ssralg]
GRing.Algebra.clone [definition, in ssralg]
GRing.Algebra.eqType [definition, in ssralg]
GRing.Algebra.lmoduleType [definition, in ssralg]
GRing.Algebra.ncalgebraType [definition, in ssralg]
GRing.Algebra.pack [definition, in ssralg]
GRing.Algebra.Pack [constructor, in ssralg]
GRing.Algebra.ringType [definition, in ssralg]
GRing.Algebra.sort [projection, in ssralg]
GRing.Algebra.type [record, in ssralg]
GRing.Algebra.zmodType [definition, in ssralg]
GRing.And [constructor, in ssralg]
GRing.and_dnf [definition, in ssralg]
GRing.and_dnfP [lemma, in ssralg]
GRing.bin_lt_charf_0 [lemma, in ssralg]
GRing.Bool [constructor, in ssralg]
GRing.cat_dnfP [lemma, in ssralg]
GRing.char [definition, in ssralg]
GRing.charf'_nat [lemma, in ssralg]
GRing.charf0 [lemma, in ssralg]
GRing.charf0P [lemma, in ssralg]
GRing.charf_eq [lemma, in ssralg]
GRing.charf_prime [lemma, in ssralg]
GRing.ClosedFieldTheory [section, in ssralg]
GRing.ClosedFieldTheory.F [variable, in ssralg]
GRing.ClosedField.axiom [definition, in ssralg]
GRing.ClosedField.base [projection, in ssralg]
GRing.ClosedField.choiceType [definition, in ssralg]
GRing.ClosedField.class [definition, in ssralg]
GRing.ClosedField.Class [constructor, in ssralg]
GRing.ClosedField.class_of [record, in ssralg]
GRing.ClosedField.clone [definition, in ssralg]
GRing.ClosedField.comRingType [definition, in ssralg]
GRing.ClosedField.comUnitRingType [definition, in ssralg]
GRing.ClosedField.decFieldType [definition, in ssralg]
GRing.ClosedField.eqType [definition, in ssralg]
GRing.ClosedField.fieldType [definition, in ssralg]
GRing.ClosedField.idomainType [definition, in ssralg]
GRing.ClosedField.Pack [constructor, in ssralg]
GRing.ClosedField.pack [definition, in ssralg]
GRing.ClosedField.ringType [definition, in ssralg]
GRing.ClosedField.sort [projection, in ssralg]
GRing.ClosedField.type [record, in ssralg]
GRing.ClosedField.unitRingType [definition, in ssralg]
GRing.ClosedField.zmodType [definition, in ssralg]
GRing.comm [abbreviation, in ssralg]
GRing.comm [abbreviation, in ssralg]
GRing.commDef [definition, in ssralg]
GRing.commrN1 [lemma, in ssralg]
GRing.commr0 [lemma, in ssralg]
GRing.commr1 [lemma, in ssralg]
GRing.commr_add [lemma, in ssralg]
GRing.commr_exp [lemma, in ssralg]
GRing.commr_exp_mull [lemma, in ssralg]
GRing.commr_inv [lemma, in ssralg]
GRing.commr_mul [lemma, in ssralg]
GRing.commr_muln [lemma, in ssralg]
GRing.commr_nat [lemma, in ssralg]
GRing.commr_opp [lemma, in ssralg]
GRing.commr_refl [lemma, in ssralg]
GRing.commr_sign [lemma, in ssralg]
GRing.commr_sym [lemma, in ssralg]
GRing.commr_unit_mul [lemma, in ssralg]
GRing.comp_ringM [lemma, in ssralg]
GRing.ComRingTheory [section, in ssralg]
GRing.ComRingTheory.R [variable, in ssralg]
GRing.ComRing.base [projection, in ssralg]
GRing.ComRing.choiceType [definition, in ssralg]
GRing.ComRing.Class [constructor, in ssralg]
GRing.ComRing.class [definition, in ssralg]
GRing.ComRing.class_of [record, in ssralg]
GRing.ComRing.clone [definition, in ssralg]
GRing.ComRing.eqType [definition, in ssralg]
GRing.ComRing.Pack [constructor, in ssralg]
GRing.ComRing.pack [definition, in ssralg]
GRing.ComRing.RingMixin [definition, in ssralg]
GRing.ComRing.ringType [definition, in ssralg]
GRing.ComRing.sort [projection, in ssralg]
GRing.ComRing.type [record, in ssralg]
GRing.ComRing.zmodType [definition, in ssralg]
GRing.ComUnitRingTheory [section, in ssralg]
GRing.ComUnitRingTheory.R [variable, in ssralg]
GRing.ComUnitRing.base1 [projection, in ssralg]
GRing.ComUnitRing.base2 [definition, in ssralg]
GRing.ComUnitRing.choiceType [definition, in ssralg]
GRing.ComUnitRing.Class [constructor, in ssralg]
GRing.ComUnitRing.class [definition, in ssralg]
GRing.ComUnitRing.class_of [record, in ssralg]
GRing.ComUnitRing.comRingType [definition, in ssralg]
GRing.ComUnitRing.com_unitRingType [definition, in ssralg]
GRing.ComUnitRing.eqType [definition, in ssralg]
GRing.ComUnitRing.ext [projection, in ssralg]
GRing.ComUnitRing.Mixin [section, in ssralg]
GRing.ComUnitRing.Mixin [definition, in ssralg]
GRing.ComUnitRing.Mixin.inv [variable, in ssralg]
GRing.ComUnitRing.Mixin.mulVx [variable, in ssralg]
GRing.ComUnitRing.Mixin.R [variable, in ssralg]
GRing.ComUnitRing.Mixin.unit [variable, in ssralg]
GRing.ComUnitRing.Mixin.unitPl [variable, in ssralg]
GRing.ComUnitRing.mulC_mulrV [lemma, in ssralg]
GRing.ComUnitRing.mulC_unitP [lemma, in ssralg]
GRing.ComUnitRing.Pack [constructor, in ssralg]
GRing.ComUnitRing.pack [definition, in ssralg]
GRing.ComUnitRing.ringType [definition, in ssralg]
GRing.ComUnitRing.sort [projection, in ssralg]
GRing.ComUnitRing.type [record, in ssralg]
GRing.ComUnitRing.unitRingType [definition, in ssralg]
GRing.ComUnitRing.zmodType [definition, in ssralg]
GRing.Const [constructor, in ssralg]
GRing.DecidableFieldTheory [section, in ssralg]
GRing.DecidableFieldTheory.F [variable, in ssralg]
GRing.DecidableField.axiom [definition, in ssralg]
GRing.DecidableField.base [projection, in ssralg]
GRing.DecidableField.choiceType [definition, in ssralg]
GRing.DecidableField.Class [constructor, in ssralg]
GRing.DecidableField.class [definition, in ssralg]
GRing.DecidableField.class_of [record, in ssralg]
GRing.DecidableField.clone [definition, in ssralg]
GRing.DecidableField.comRingType [definition, in ssralg]
GRing.DecidableField.comUnitRingType [definition, in ssralg]
GRing.DecidableField.eqType [definition, in ssralg]
GRing.DecidableField.fieldType [definition, in ssralg]
GRing.DecidableField.idomainType [definition, in ssralg]
GRing.DecidableField.Mixin [constructor, in ssralg]
GRing.DecidableField.mixin [projection, in ssralg]
GRing.DecidableField.mixin_of [record, in ssralg]
GRing.DecidableField.Pack [constructor, in ssralg]
GRing.DecidableField.pack [definition, in ssralg]
GRing.DecidableField.ringType [definition, in ssralg]
GRing.DecidableField.sat [projection, in ssralg]
GRing.DecidableField.satP [projection, in ssralg]
GRing.DecidableField.sort [projection, in ssralg]
GRing.DecidableField.type [record, in ssralg]
GRing.DecidableField.unitRingType [definition, in ssralg]
GRing.DecidableField.zmodType [definition, in ssralg]
GRing.divff [lemma, in ssralg]
GRing.divfK [definition, in ssralg]
GRing.divrK [definition, in ssralg]
GRing.divrr [lemma, in ssralg]
GRing.dnf_rterm [definition, in ssralg]
GRing.dnf_to_form [definition, in ssralg]
GRing.dnf_to_form_qf [lemma, in ssralg]
GRing.dnf_to_rform [lemma, in ssralg]
GRing.dvdn_charf [lemma, in ssralg]
GRing.elim_aux [definition, in ssralg]
GRing.Equal [constructor, in ssralg]
GRing.eq0_rform [definition, in ssralg]
GRing.eq_eval [lemma, in ssralg]
GRing.eq_holds [lemma, in ssralg]
GRing.eq_sat [lemma, in ssralg]
GRing.eq_sol [lemma, in ssralg]
GRing.eval [definition, in ssralg]
GRing.EvalTerm [section, in ssralg]
GRing.EvalTerm.MultiQuant [section, in ssralg]
GRing.EvalTerm.MultiQuant.f [variable, in ssralg]
GRing.EvalTerm.Pick [section, in ssralg]
GRing.EvalTerm.Pick.else_f [variable, in ssralg]
GRing.EvalTerm.Pick.I [variable, in ssralg]
GRing.EvalTerm.Pick.pred_f [variable, in ssralg]
GRing.EvalTerm.Pick.then_f [variable, in ssralg]
GRing.EvalTerm.R [variable, in ssralg]
GRing.eval_Pick [lemma, in ssralg]
GRing.eval_tsubst [lemma, in ssralg]
GRing.Exists [constructor, in ssralg]
GRing.exp [definition, in ssralg]
GRing.Exp [constructor, in ssralg]
GRing.expf_eq0 [lemma, in ssralg]
GRing.expf_neq0 [lemma, in ssralg]
GRing.exprN [lemma, in ssralg]
GRing.exprn_addl [lemma, in ssralg]
GRing.exprn_addl_comm [lemma, in ssralg]
GRing.exprn_addr [lemma, in ssralg]
GRing.exprn_mull [lemma, in ssralg]
GRing.exprn_mulnl [lemma, in ssralg]
GRing.exprn_mulr [lemma, in ssralg]
GRing.exprn_subl [lemma, in ssralg]
GRing.exprn_subl_comm [lemma, in ssralg]
GRing.exprS [lemma, in ssralg]
GRing.exprSr [lemma, in ssralg]
GRing.expr0 [lemma, in ssralg]
GRing.expr1 [lemma, in ssralg]
GRing.expr_inv [lemma, in ssralg]
GRing.exp1rn [lemma, in ssralg]
GRing.False [abbreviation, in ssralg]
GRing.fE [abbreviation, in ssralg]
GRing.fieldM_char [lemma, in ssralg]
GRing.fieldM_div [lemma, in ssralg]
GRing.fieldM_eq0 [lemma, in ssralg]
GRing.fieldM_inj [lemma, in ssralg]
GRing.fieldM_inv [lemma, in ssralg]
GRing.fieldM_unit [lemma, in ssralg]
GRing.FieldTheory [section, in ssralg]
GRing.FieldTheory.F [variable, in ssralg]
GRing.FieldTheory.FieldMorphismInj [section, in ssralg]
GRing.FieldTheory.FieldMorphismInj.f [variable, in ssralg]
GRing.FieldTheory.FieldMorphismInj.fRM [variable, in ssralg]
GRing.FieldTheory.FieldMorphismInj.R [variable, in ssralg]
GRing.FieldTheory.FieldMorphismInv [section, in ssralg]
GRing.FieldTheory.FieldMorphismInv.f [variable, in ssralg]
GRing.FieldTheory.FieldMorphismInv.fRM [variable, in ssralg]
GRing.FieldTheory.FieldMorphismInv.R [variable, in ssralg]
GRing.Field.axiom [definition, in ssralg]
GRing.Field.base [projection, in ssralg]
GRing.Field.choiceType [definition, in ssralg]
GRing.Field.Class [constructor, in ssralg]
GRing.Field.class [definition, in ssralg]
GRing.Field.class_of [record, in ssralg]
GRing.Field.clone [definition, in ssralg]
GRing.Field.comRingType [definition, in ssralg]
GRing.Field.comUnitRingType [definition, in ssralg]
GRing.Field.eqType [definition, in ssralg]
GRing.Field.ext [projection, in ssralg]
GRing.Field.IdomainMixin [lemma, in ssralg]
GRing.Field.idomainType [definition, in ssralg]
GRing.Field.intro_unit [lemma, in ssralg]
GRing.Field.inv_out [lemma, in ssralg]
GRing.Field.Mixin [lemma, in ssralg]
GRing.Field.Mixins [section, in ssralg]
GRing.Field.Mixins.inv [variable, in ssralg]
GRing.Field.Mixins.inv0 [variable, in ssralg]
GRing.Field.Mixins.mulVx [variable, in ssralg]
GRing.Field.Mixins.R [variable, in ssralg]
GRing.Field.mixin_of [definition, in ssralg]
GRing.Field.pack [definition, in ssralg]
GRing.Field.Pack [constructor, in ssralg]
GRing.Field.ringType [definition, in ssralg]
GRing.Field.sort [projection, in ssralg]
GRing.Field.type [record, in ssralg]
GRing.Field.UnitMixin [definition, in ssralg]
GRing.Field.unitRingType [definition, in ssralg]
GRing.Field.zmodType [definition, in ssralg]
GRing.foldExistsP [lemma, in ssralg]
GRing.foldForallP [lemma, in ssralg]
GRing.Forall [constructor, in ssralg]
GRing.formula [inductive, in ssralg]
GRing.Frobenius_aut [definition, in ssralg]
GRing.Frobenius_autE [lemma, in ssralg]
GRing.Frobenius_aut_add_comm [lemma, in ssralg]
GRing.Frobenius_aut_exp [lemma, in ssralg]
GRing.Frobenius_aut_muln [lemma, in ssralg]
GRing.Frobenius_aut_mul_comm [lemma, in ssralg]
GRing.Frobenius_aut_nat [lemma, in ssralg]
GRing.Frobenius_aut_opp [lemma, in ssralg]
GRing.Frobenius_aut_RM [lemma, in ssralg]
GRing.Frobenius_aut_sub_comm [lemma, in ssralg]
GRing.Frobenius_aut_0 [lemma, in ssralg]
GRing.Frobenius_aut_1 [lemma, in ssralg]
GRing.fsubst [definition, in ssralg]
GRing.holds [definition, in ssralg]
GRing.holds_fsubst [lemma, in ssralg]
GRing.holds_proj [lemma, in ssralg]
GRing.Implies [constructor, in ssralg]
GRing.IntegralDomainTheory [section, in ssralg]
GRing.IntegralDomainTheory.R [variable, in ssralg]
GRing.IntegralDomain.axiom [definition, in ssralg]
GRing.IntegralDomain.base [projection, in ssralg]
GRing.IntegralDomain.choiceType [definition, in ssralg]
GRing.IntegralDomain.Class [constructor, in ssralg]
GRing.IntegralDomain.class [definition, in ssralg]
GRing.IntegralDomain.class_of [record, in ssralg]
GRing.IntegralDomain.clone [definition, in ssralg]
GRing.IntegralDomain.comRingType [definition, in ssralg]
GRing.IntegralDomain.comUnitRingType [definition, in ssralg]
GRing.IntegralDomain.eqType [definition, in ssralg]
GRing.IntegralDomain.ext [projection, in ssralg]
GRing.IntegralDomain.Pack [constructor, in ssralg]
GRing.IntegralDomain.pack [definition, in ssralg]
GRing.IntegralDomain.ringType [definition, in ssralg]
GRing.IntegralDomain.sort [projection, in ssralg]
GRing.IntegralDomain.type [record, in ssralg]
GRing.IntegralDomain.unitRingType [definition, in ssralg]
GRing.IntegralDomain.zmodType [definition, in ssralg]
GRing.Inv [constructor, in ssralg]
GRing.inv [definition, in ssralg]
GRing.invf_mul [lemma, in ssralg]
GRing.invrK [lemma, in ssralg]
GRing.invrN [lemma, in ssralg]
GRing.invr0 [lemma, in ssralg]
GRing.invr1 [lemma, in ssralg]
GRing.invr_eq0 [lemma, in ssralg]
GRing.invr_inj [lemma, in ssralg]
GRing.invr_mul [lemma, in ssralg]
GRing.invr_neq0 [lemma, in ssralg]
GRing.invr_out [lemma, in ssralg]
GRing.LmoduleTheory [section, in ssralg]
GRing.LmoduleTheory.M [variable, in ssralg]
GRing.LmoduleTheory.R [variable, in ssralg]
GRing.Lmodule.base [projection, in ssralg]
GRing.Lmodule.choiceType [definition, in ssralg]
GRing.Lmodule.Class [constructor, in ssralg]
GRing.Lmodule.class [definition, in ssralg]
GRing.Lmodule.class_of [record, in ssralg]
GRing.Lmodule.clone [definition, in ssralg]
GRing.Lmodule.eqType [definition, in ssralg]
GRing.Lmodule.ext [projection, in ssralg]
GRing.Lmodule.Lmodule [section, in ssralg]
GRing.Lmodule.Lmodule.R [variable, in ssralg]
GRing.Lmodule.Mixin [constructor, in ssralg]
GRing.Lmodule.mixin_of [record, in ssralg]
GRing.Lmodule.pack [definition, in ssralg]
GRing.Lmodule.Pack [constructor, in ssralg]
GRing.Lmodule.scale [projection, in ssralg]
GRing.Lmodule.sort [projection, in ssralg]
GRing.Lmodule.type [record, in ssralg]
GRing.Lmodule.zmodType [definition, in ssralg]
GRing.morphism [definition, in ssralg]
GRing.morph_sunit [lemma, in ssralg]
GRing.mul [definition, in ssralg]
GRing.Mul [constructor, in ssralg]
GRing.mulfI [lemma, in ssralg]
GRing.mulfK [lemma, in ssralg]
GRing.mulfV [definition, in ssralg]
GRing.mulfVK [lemma, in ssralg]
GRing.mulf_eq0 [lemma, in ssralg]
GRing.mulf_neq0 [lemma, in ssralg]
GRing.mulIf [lemma, in ssralg]
GRing.mulIr [lemma, in ssralg]
GRing.mulKf [lemma, in ssralg]
GRing.mulKr [lemma, in ssralg]
GRing.mulNr [lemma, in ssralg]
GRing.mulN1r [lemma, in ssralg]
GRing.muloid [definition, in ssralg]
GRing.mulrA [lemma, in ssralg]
GRing.mulrAC [lemma, in ssralg]
GRing.mulrb [lemma, in ssralg]
GRing.mulrC [lemma, in ssralg]
GRing.mulrCA [lemma, in ssralg]
GRing.mulrI [lemma, in ssralg]
GRing.mulrK [lemma, in ssralg]
GRing.mulrN [lemma, in ssralg]
GRing.mulrnA [lemma, in ssralg]
GRing.mulrnAC [lemma, in ssralg]
GRing.mulrnAl [lemma, in ssralg]
GRing.mulrnAr [lemma, in ssralg]
GRing.mulrNN [lemma, in ssralg]
GRing.mulrN1 [lemma, in ssralg]
GRing.mulrn_addl [lemma, in ssralg]
GRing.mulrn_addr [lemma, in ssralg]
GRing.mulrS [lemma, in ssralg]
GRing.mulrSr [lemma, in ssralg]
GRing.mulrV [definition, in ssralg]
GRing.mulrVK [lemma, in ssralg]
GRing.mulr0 [lemma, in ssralg]
GRing.mulr0n [lemma, in ssralg]
GRing.mulr1 [lemma, in ssralg]
GRing.mulr1n [lemma, in ssralg]
GRing.mulr_addl [lemma, in ssralg]
GRing.mulr_addr [lemma, in ssralg]
GRing.mulr_natl [lemma, in ssralg]
GRing.mulr_natr [lemma, in ssralg]
GRing.mulr_subl [lemma, in ssralg]
GRing.mulr_subr [lemma, in ssralg]
GRing.mulVf [lemma, in ssralg]
GRing.mulVKf [lemma, in ssralg]
GRing.mulVKr [lemma, in ssralg]
GRing.mulVr [lemma, in ssralg]
GRing.mul0r [lemma, in ssralg]
GRing.mul0rn [lemma, in ssralg]
GRing.mul1r [lemma, in ssralg]
GRing.mul_comoid [definition, in ssralg]
GRing.mul_monoid [definition, in ssralg]
GRing.NatConst [constructor, in ssralg]
GRing.natf0_char [lemma, in ssralg]
GRing.NatMul [constructor, in ssralg]
GRing.natmul [definition, in ssralg]
GRing.natr_add [lemma, in ssralg]
GRing.natr_exp [lemma, in ssralg]
GRing.natr_mul [lemma, in ssralg]
GRing.NCalgebraTheory [section, in ssralg]
GRing.NCalgebraTheory.A [variable, in ssralg]
GRing.NCalgebraTheory.R [variable, in ssralg]
GRing.NCalgebra.axiom [definition, in ssralg]
GRing.NCalgebra.base1 [projection, in ssralg]
GRing.NCalgebra.base2 [definition, in ssralg]
GRing.NCalgebra.choiceType [definition, in ssralg]
GRing.NCalgebra.Class [constructor, in ssralg]
GRing.NCalgebra.class [definition, in ssralg]
GRing.NCalgebra.class_of [record, in ssralg]
GRing.NCalgebra.clone [definition, in ssralg]
GRing.NCalgebra.eqType [definition, in ssralg]
GRing.NCalgebra.ext [projection, in ssralg]
GRing.NCalgebra.lmoduleType [definition, in ssralg]
GRing.NCalgebra.lmod_ringType [definition, in ssralg]
GRing.NCalgebra.mixin [projection, in ssralg]
GRing.NCalgebra.NCalgebra [section, in ssralg]
GRing.NCalgebra.NCalgebra.R [variable, in ssralg]
GRing.NCalgebra.pack [definition, in ssralg]
GRing.NCalgebra.Pack [constructor, in ssralg]
GRing.NCalgebra.ringType [definition, in ssralg]
GRing.NCalgebra.scale [abbreviation, in ssralg]
GRing.NCalgebra.sort [projection, in ssralg]
GRing.NCalgebra.type [record, in ssralg]
GRing.NCalgebra.zmodType [definition, in ssralg]
GRing.nonzero1r [lemma, in ssralg]
GRing.Not [constructor, in ssralg]
GRing.one [definition, in ssralg]
GRing.oner_eq0 [lemma, in ssralg]
GRing.Opp [constructor, in ssralg]
GRing.opp [definition, in ssralg]
GRing.opprK [lemma, in ssralg]
GRing.oppr0 [lemma, in ssralg]
GRing.oppr_add [lemma, in ssralg]
GRing.oppr_eq0 [lemma, in ssralg]
GRing.oppr_muln [lemma, in ssralg]
GRing.oppr_sub [lemma, in ssralg]
GRing.Or [constructor, in ssralg]
GRing.Pick [definition, in ssralg]
GRing.Pick_form_qf [lemma, in ssralg]
GRing.prodf_inv [lemma, in ssralg]
GRing.prodr_const [lemma, in ssralg]
GRing.prodr_exp [lemma, in ssralg]
GRing.prodr_exp_r [lemma, in ssralg]
GRing.prodr_opp [lemma, in ssralg]
GRing.proj [definition, in ssralg]
GRing.proj_sat [definition, in ssralg]
GRing.proj_satP [lemma, in ssralg]
GRing.QEDecidableField [definition, in ssralg]
GRing.QEDecidableFieldMixin [definition, in ssralg]
GRing.QE.Axioms [section, in ssralg]
GRing.QE.Axioms.proj [variable, in ssralg]
GRing.QE.Axioms.R [variable, in ssralg]
GRing.QE.base [projection, in ssralg]
GRing.QE.choiceType [definition, in ssralg]
GRing.QE.Class [constructor, in ssralg]
GRing.QE.class [definition, in ssralg]
GRing.QE.class_of [record, in ssralg]
GRing.QE.clone [definition, in ssralg]
GRing.QE.comRingType [definition, in ssralg]
GRing.QE.comUnitRingType [definition, in ssralg]
GRing.QE.eqType [definition, in ssralg]
GRing.QE.fieldType [definition, in ssralg]
GRing.QE.holds_proj [projection, in ssralg]
GRing.QE.holds_proj_axiom [definition, in ssralg]
GRing.QE.idomainType [definition, in ssralg]
GRing.QE.Mixin [constructor, in ssralg]
GRing.QE.mixin [projection, in ssralg]
GRing.QE.mixin_of [record, in ssralg]
GRing.QE.Pack [constructor, in ssralg]
GRing.QE.pack [definition, in ssralg]
GRing.QE.proj [projection, in ssralg]
GRing.QE.ringType [definition, in ssralg]
GRing.QE.sort [projection, in ssralg]
GRing.QE.type [record, in ssralg]
GRing.QE.unitRingType [definition, in ssralg]
GRing.QE.wf_proj [projection, in ssralg]
GRing.QE.wf_proj_axiom [definition, in ssralg]
GRing.QE.zmodType [definition, in ssralg]
GRing.QE_theory [section, in ssralg]
GRing.QE_theory.F [variable, in ssralg]
GRing.qf_eval [definition, in ssralg]
GRing.qf_evalP [lemma, in ssralg]
GRing.qf_form [definition, in ssralg]
GRing.qf_to_dnf [definition, in ssralg]
GRing.qf_to_dnfP [lemma, in ssralg]
GRing.qf_to_dnf_rterm [lemma, in ssralg]
GRing.quantifier_elim [definition, in ssralg]
GRing.quantifier_elim_rformP [lemma, in ssralg]
GRing.quantifier_elim_wf [lemma, in ssralg]
GRing.rev [abbreviation, in ssralg]
GRing.RevRingMixin [definition, in ssralg]
GRing.RevRingType [definition, in ssralg]
GRing.rformula [definition, in ssralg]
GRing.RingMorphTheory [section, in ssralg]
GRing.RingMorphTheory.aR [variable, in ssralg]
GRing.RingMorphTheory.aR' [variable, in ssralg]
GRing.RingMorphTheory.f [variable, in ssralg]
GRing.RingMorphTheory.fM [variable, in ssralg]
GRing.RingMorphTheory.g [variable, in ssralg]
GRing.RingMorphTheory.gM [variable, in ssralg]
GRing.RingMorphTheory.rR [variable, in ssralg]
GRing.ringM_add [lemma, in ssralg]
GRing.ringM_char [lemma, in ssralg]
GRing.ringM_comm [lemma, in ssralg]
GRing.ringM_div [lemma, in ssralg]
GRing.ringM_exp [lemma, in ssralg]
GRing.ringM_inv [lemma, in ssralg]
GRing.ringM_isom [lemma, in ssralg]
GRing.ringM_mul [lemma, in ssralg]
GRing.ringM_nat [lemma, in ssralg]
GRing.ringM_natmul [lemma, in ssralg]
GRing.ringM_opp [lemma, in ssralg]
GRing.ringM_prod [definition, in ssralg]
GRing.ringM_sign [lemma, in ssralg]
GRing.ringM_sub [lemma, in ssralg]
GRing.ringM_sum [definition, in ssralg]
GRing.ringM_unit [lemma, in ssralg]
GRing.ringM_0 [lemma, in ssralg]
GRing.ringM_1 [lemma, in ssralg]
GRing.RingTheory [section, in ssralg]
GRing.RingTheory.Frobenius [section, in ssralg]
GRing.RingTheory.Frobenius.charFp [variable, in ssralg]
GRing.RingTheory.Frobenius.p [variable, in ssralg]
GRing.RingTheory.R [variable, in ssralg]
GRing.Ring.base [projection, in ssralg]
GRing.Ring.choiceType [definition, in ssralg]
GRing.Ring.Class [constructor, in ssralg]
GRing.Ring.class [definition, in ssralg]
GRing.Ring.class_of [record, in ssralg]
GRing.Ring.clone [definition, in ssralg]
GRing.Ring.eqType [definition, in ssralg]
GRing.Ring.EtaMixin [definition, in ssralg]
GRing.Ring.ext [projection, in ssralg]
GRing.Ring.Mixin [constructor, in ssralg]
GRing.Ring.mixin_of [record, in ssralg]
GRing.Ring.mul [projection, in ssralg]
GRing.Ring.one [projection, in ssralg]
GRing.Ring.pack [definition, in ssralg]
GRing.Ring.Pack [constructor, in ssralg]
GRing.Ring.sort [projection, in ssralg]
GRing.Ring.type [record, in ssralg]
GRing.Ring.zmodType [definition, in ssralg]
GRing.rterm [definition, in ssralg]
GRing.same_env [definition, in ssralg]
GRing.same_env_sym [lemma, in ssralg]
GRing.sat [definition, in ssralg]
GRing.satP [lemma, in ssralg]
GRing.scale [definition, in ssralg]
GRing.scaleNr [lemma, in ssralg]
GRing.scaleN1r [lemma, in ssralg]
GRing.scalerA [lemma, in ssralg]
GRing.scalerN [lemma, in ssralg]
GRing.scaler0 [lemma, in ssralg]
GRing.scaler_addl [lemma, in ssralg]
GRing.scaler_addr [lemma, in ssralg]
GRing.scaler_com [lemma, in ssralg]
GRing.scaler_mull [lemma, in ssralg]
GRing.scaler_nat [lemma, in ssralg]
GRing.scaler_subl [lemma, in ssralg]
GRing.scaler_subr [lemma, in ssralg]
GRing.scaler_suml [lemma, in ssralg]
GRing.scaler_sumr [lemma, in ssralg]
GRing.scale0r [lemma, in ssralg]
GRing.scale1r [lemma, in ssralg]
GRing.signr_addb [lemma, in ssralg]
GRing.signr_eq0 [lemma, in ssralg]
GRing.signr_odd [lemma, in ssralg]
GRing.size_sol [lemma, in ssralg]
GRing.sol [definition, in ssralg]
GRing.solP [lemma, in ssralg]
GRing.solve_monicpoly [lemma, in ssralg]
GRing.sol_subproof [lemma, in ssralg]
GRing.subrK [definition, in ssralg]
GRing.subrr [definition, in ssralg]
GRing.subr0 [lemma, in ssralg]
GRing.subr_eq [lemma, in ssralg]
GRing.subr_eq0 [lemma, in ssralg]
GRing.subr_expn [lemma, in ssralg]
GRing.subr_expn_comm [lemma, in ssralg]
GRing.subr_expn_1 [lemma, in ssralg]
GRing.Substitution [section, in ssralg]
GRing.Substitution.R [variable, in ssralg]
GRing.sub0r [lemma, in ssralg]
GRing.sumr_const [lemma, in ssralg]
GRing.sumr_muln [lemma, in ssralg]
GRing.sumr_muln_r [lemma, in ssralg]
GRing.sumr_opp [lemma, in ssralg]
GRing.sumr_sub [lemma, in ssralg]
GRing.term [inductive, in ssralg]
GRing.TermDef [section, in ssralg]
GRing.TermDef.R [variable, in ssralg]
GRing.Theory.addIr [definition, in ssralg]
GRing.Theory.addKr [definition, in ssralg]
GRing.Theory.addNKr [definition, in ssralg]
GRing.Theory.addNr [definition, in ssralg]
GRing.Theory.addrA [definition, in ssralg]
GRing.Theory.addrAC [definition, in ssralg]
GRing.Theory.addrC [definition, in ssralg]
GRing.Theory.addrCA [definition, in ssralg]
GRing.Theory.addrI [definition, in ssralg]
GRing.Theory.addrK [definition, in ssralg]
GRing.Theory.addrN [definition, in ssralg]
GRing.Theory.addrNK [definition, in ssralg]
GRing.Theory.addr0 [definition, in ssralg]
GRing.Theory.add0r [definition, in ssralg]
GRing.Theory.bin_lt_charf_0 [definition, in ssralg]
GRing.Theory.charf'_nat [definition, in ssralg]
GRing.Theory.charf0 [definition, in ssralg]
GRing.Theory.charf0P [definition, in ssralg]
GRing.Theory.charf_eq [definition, in ssralg]
GRing.Theory.charf_prime [definition, in ssralg]
GRing.Theory.commrN1 [definition, in ssralg]
GRing.Theory.commr0 [definition, in ssralg]
GRing.Theory.commr1 [definition, in ssralg]
GRing.Theory.commr_add [definition, in ssralg]
GRing.Theory.commr_exp [definition, in ssralg]
GRing.Theory.commr_exp_mull [definition, in ssralg]
GRing.Theory.commr_inv [definition, in ssralg]
GRing.Theory.commr_mul [definition, in ssralg]
GRing.Theory.commr_muln [definition, in ssralg]
GRing.Theory.commr_nat [definition, in ssralg]
GRing.Theory.commr_opp [definition, in ssralg]
GRing.Theory.commr_refl [definition, in ssralg]
GRing.Theory.commr_sign [definition, in ssralg]
GRing.Theory.commr_sym [definition, in ssralg]
GRing.Theory.commr_unit_mul [definition, in ssralg]
GRing.Theory.comp_ringM [definition, in ssralg]
GRing.Theory.divff [definition, in ssralg]
GRing.Theory.divfK [definition, in ssralg]
GRing.Theory.divrK [definition, in ssralg]
GRing.Theory.divrr [definition, in ssralg]
GRing.Theory.dvdn_charf [definition, in ssralg]
GRing.Theory.eq_eval [definition, in ssralg]
GRing.Theory.eq_holds [definition, in ssralg]
GRing.Theory.eq_sat [definition, in ssralg]
GRing.Theory.eq_sol [definition, in ssralg]
GRing.Theory.eval_tsubst [definition, in ssralg]
GRing.Theory.expf_eq0 [definition, in ssralg]
GRing.Theory.expf_neq0 [definition, in ssralg]
GRing.Theory.exprN [definition, in ssralg]
GRing.Theory.exprn_addl [definition, in ssralg]
GRing.Theory.exprn_addl_comm [definition, in ssralg]
GRing.Theory.exprn_addr [definition, in ssralg]
GRing.Theory.exprn_mull [definition, in ssralg]
GRing.Theory.exprn_mulnl [definition, in ssralg]
GRing.Theory.exprn_mulr [definition, in ssralg]
GRing.Theory.exprn_subl [definition, in ssralg]
GRing.Theory.exprn_subl_comm [definition, in ssralg]
GRing.Theory.exprS [definition, in ssralg]
GRing.Theory.exprSr [definition, in ssralg]
GRing.Theory.expr0 [definition, in ssralg]
GRing.Theory.expr1 [definition, in ssralg]
GRing.Theory.expr_inv [definition, in ssralg]
GRing.Theory.exp1rn [definition, in ssralg]
GRing.Theory.fieldM_char [definition, in ssralg]
GRing.Theory.fieldM_div [definition, in ssralg]
GRing.Theory.fieldM_eq0 [definition, in ssralg]
GRing.Theory.fieldM_inj [definition, in ssralg]
GRing.Theory.fieldM_inv [definition, in ssralg]
GRing.Theory.fieldM_unit [definition, in ssralg]
GRing.Theory.Frobenius_autE [definition, in ssralg]
GRing.Theory.Frobenius_aut_add_comm [definition, in ssralg]
GRing.Theory.Frobenius_aut_exp [definition, in ssralg]
GRing.Theory.Frobenius_aut_muln [definition, in ssralg]
GRing.Theory.Frobenius_aut_mul_comm [definition, in ssralg]
GRing.Theory.Frobenius_aut_nat [definition, in ssralg]
GRing.Theory.Frobenius_aut_opp [definition, in ssralg]
GRing.Theory.Frobenius_aut_RM [definition, in ssralg]
GRing.Theory.Frobenius_aut_sub_comm [definition, in ssralg]
GRing.Theory.Frobenius_aut_0 [definition, in ssralg]
GRing.Theory.Frobenius_aut_1 [definition, in ssralg]
GRing.Theory.holds_fsubst [definition, in ssralg]
GRing.Theory.invf_mul [definition, in ssralg]
GRing.Theory.invrK [definition, in ssralg]
GRing.Theory.invrN [definition, in ssralg]
GRing.Theory.invr0 [definition, in ssralg]
GRing.Theory.invr1 [definition, in ssralg]
GRing.Theory.invr_eq0 [definition, in ssralg]
GRing.Theory.invr_inj [definition, in ssralg]
GRing.Theory.invr_mul [definition, in ssralg]
GRing.Theory.invr_neq0 [definition, in ssralg]
GRing.Theory.invr_out [definition, in ssralg]
GRing.Theory.morph_sunit [definition, in ssralg]
GRing.Theory.mulfI [definition, in ssralg]
GRing.Theory.mulfK [definition, in ssralg]
GRing.Theory.mulfV [definition, in ssralg]
GRing.Theory.mulfVK [definition, in ssralg]
GRing.Theory.mulf_eq0 [definition, in ssralg]
GRing.Theory.mulf_neq0 [definition, in ssralg]
GRing.Theory.mulIf [definition, in ssralg]
GRing.Theory.mulIr [definition, in ssralg]
GRing.Theory.mulKf [definition, in ssralg]
GRing.Theory.mulKr [definition, in ssralg]
GRing.Theory.mulNr [definition, in ssralg]
GRing.Theory.mulN1r [definition, in ssralg]
GRing.Theory.mulrA [definition, in ssralg]
GRing.Theory.mulrAC [definition, in ssralg]
GRing.Theory.mulrb [definition, in ssralg]
GRing.Theory.mulrC [definition, in ssralg]
GRing.Theory.mulrCA [definition, in ssralg]
GRing.Theory.mulrI [definition, in ssralg]
GRing.Theory.mulrK [definition, in ssralg]
GRing.Theory.mulrN [definition, in ssralg]
GRing.Theory.mulrnA [definition, in ssralg]
GRing.Theory.mulrnAC [definition, in ssralg]
GRing.Theory.mulrnAl [definition, in ssralg]
GRing.Theory.mulrnAr [definition, in ssralg]
GRing.Theory.mulrNN [definition, in ssralg]
GRing.Theory.mulrN1 [definition, in ssralg]
GRing.Theory.mulrn_addl [definition, in ssralg]
GRing.Theory.mulrn_addr [definition, in ssralg]
GRing.Theory.mulrS [definition, in ssralg]
GRing.Theory.mulrSr [definition, in ssralg]
GRing.Theory.mulrV [definition, in ssralg]
GRing.Theory.mulrVK [definition, in ssralg]
GRing.Theory.mulr0 [definition, in ssralg]
GRing.Theory.mulr0n [definition, in ssralg]
GRing.Theory.mulr1 [definition, in ssralg]
GRing.Theory.mulr1n [definition, in ssralg]
GRing.Theory.mulr_addl [definition, in ssralg]
GRing.Theory.mulr_addr [definition, in ssralg]
GRing.Theory.mulr_natl [definition, in ssralg]
GRing.Theory.mulr_natr [definition, in ssralg]
GRing.Theory.mulr_subl [definition, in ssralg]
GRing.Theory.mulr_subr [definition, in ssralg]
GRing.Theory.mulVf [definition, in ssralg]
GRing.Theory.mulVKf [definition, in ssralg]
GRing.Theory.mulVKr [definition, in ssralg]
GRing.Theory.mulVr [definition, in ssralg]
GRing.Theory.mul0r [definition, in ssralg]
GRing.Theory.mul0rn [definition, in ssralg]
GRing.Theory.mul1r [definition, in ssralg]
GRing.Theory.natf0_char [definition, in ssralg]
GRing.Theory.natr_add [definition, in ssralg]
GRing.Theory.natr_exp [definition, in ssralg]
GRing.Theory.natr_mul [definition, in ssralg]
GRing.Theory.nonzero1r [definition, in ssralg]
GRing.Theory.oner_eq0 [definition, in ssralg]
GRing.Theory.opprK [definition, in ssralg]
GRing.Theory.oppr0 [definition, in ssralg]
GRing.Theory.oppr_add [definition, in ssralg]
GRing.Theory.oppr_eq0 [definition, in ssralg]
GRing.Theory.oppr_muln [definition, in ssralg]
GRing.Theory.oppr_sub [definition, in ssralg]
GRing.Theory.prodf_inv [definition, in ssralg]
GRing.Theory.prodr_const [definition, in ssralg]
GRing.Theory.prodr_exp [definition, in ssralg]
GRing.Theory.prodr_exp_r [definition, in ssralg]
GRing.Theory.prodr_opp [definition, in ssralg]
GRing.Theory.ringM_add [definition, in ssralg]
GRing.Theory.ringM_char [definition, in ssralg]
GRing.Theory.ringM_comm [definition, in ssralg]
GRing.Theory.ringM_div [definition, in ssralg]
GRing.Theory.ringM_exp [definition, in ssralg]
GRing.Theory.ringM_inv [definition, in ssralg]
GRing.Theory.ringM_isom [definition, in ssralg]
GRing.Theory.ringM_mul [definition, in ssralg]
GRing.Theory.ringM_nat [definition, in ssralg]
GRing.Theory.ringM_natmul [definition, in ssralg]
GRing.Theory.ringM_opp [definition, in ssralg]
GRing.Theory.ringM_prod [definition, in ssralg]
GRing.Theory.ringM_sign [definition, in ssralg]
GRing.Theory.ringM_sub [definition, in ssralg]
GRing.Theory.ringM_sum [definition, in ssralg]
GRing.Theory.ringM_unit [definition, in ssralg]
GRing.Theory.ringM_0 [definition, in ssralg]
GRing.Theory.ringM_1 [definition, in ssralg]
GRing.Theory.satP [definition, in ssralg]
GRing.Theory.scaleNr [definition, in ssralg]
GRing.Theory.scaleN1r [definition, in ssralg]
GRing.Theory.scalerA [definition, in ssralg]
GRing.Theory.scalerN [definition, in ssralg]
GRing.Theory.scaler0 [definition, in ssralg]
GRing.Theory.scaler_addl [definition, in ssralg]
GRing.Theory.scaler_addr [definition, in ssralg]
GRing.Theory.scaler_mull [definition, in ssralg]
GRing.Theory.scaler_nat [definition, in ssralg]
GRing.Theory.scaler_subl [definition, in ssralg]
GRing.Theory.scaler_subr [definition, in ssralg]
GRing.Theory.scaler_suml [definition, in ssralg]
GRing.Theory.scaler_sumr [definition, in ssralg]
GRing.Theory.scale0r [definition, in ssralg]
GRing.Theory.scale1r [definition, in ssralg]
GRing.Theory.signr_addb [definition, in ssralg]
GRing.Theory.signr_eq0 [definition, in ssralg]
GRing.Theory.signr_odd [definition, in ssralg]
GRing.Theory.size_sol [definition, in ssralg]
GRing.Theory.solP [definition, in ssralg]
GRing.Theory.solve_monicpoly [definition, in ssralg]
GRing.Theory.subrK [definition, in ssralg]
GRing.Theory.subrr [definition, in ssralg]
GRing.Theory.subr0 [definition, in ssralg]
GRing.Theory.subr_eq [definition, in ssralg]
GRing.Theory.subr_eq0 [definition, in ssralg]
GRing.Theory.subr_expn [definition, in ssralg]
GRing.Theory.subr_expn_comm [definition, in ssralg]
GRing.Theory.subr_expn_1 [definition, in ssralg]
GRing.Theory.sub0r [definition, in ssralg]
GRing.Theory.sumr_const [definition, in ssralg]
GRing.Theory.sumr_muln [definition, in ssralg]
GRing.Theory.sumr_muln_r [definition, in ssralg]
GRing.Theory.sumr_opp [definition, in ssralg]
GRing.Theory.sumr_sub [definition, in ssralg]
GRing.Theory.unitfE [definition, in ssralg]
GRing.Theory.unitrE [definition, in ssralg]
GRing.Theory.unitrP [definition, in ssralg]
GRing.Theory.unitr0 [definition, in ssralg]
GRing.Theory.unitr1 [definition, in ssralg]
GRing.Theory.unitr_exp [definition, in ssralg]
GRing.Theory.unitr_inv [definition, in ssralg]
GRing.Theory.unitr_mul [definition, in ssralg]
GRing.Theory.unitr_mull [definition, in ssralg]
GRing.Theory.unitr_mulr [definition, in ssralg]
GRing.Theory.unitr_opp [definition, in ssralg]
GRing.Theory.unitr_pexp [definition, in ssralg]
GRing.to_rform [definition, in ssralg]
GRing.to_rformP [lemma, in ssralg]
GRing.to_rform_rformula [lemma, in ssralg]
GRing.to_rterm [definition, in ssralg]
GRing.to_rterm_id [lemma, in ssralg]
GRing.True [abbreviation, in ssralg]
GRing.tsubst [definition, in ssralg]
GRing.ub_var [definition, in ssralg]
GRing.unit [abbreviation, in ssralg]
GRing.Unit [constructor, in ssralg]
GRing.unitDef [definition, in ssralg]
GRing.unitfE [lemma, in ssralg]
GRing.unitrE [lemma, in ssralg]
GRing.UnitRingMorphism [section, in ssralg]
GRing.UnitRingMorphism.aR [variable, in ssralg]
GRing.UnitRingMorphism.f [variable, in ssralg]
GRing.UnitRingMorphism.fM [variable, in ssralg]
GRing.UnitRingMorphism.rR [variable, in ssralg]
GRing.UnitRingTheory [section, in ssralg]
GRing.UnitRingTheory.R [variable, in ssralg]
GRing.UnitRing.base [projection, in ssralg]
GRing.UnitRing.choiceType [definition, in ssralg]
GRing.UnitRing.class [definition, in ssralg]
GRing.UnitRing.Class [constructor, in ssralg]
GRing.UnitRing.class_of [record, in ssralg]
GRing.UnitRing.clone [definition, in ssralg]
GRing.UnitRing.eqType [definition, in ssralg]
GRing.UnitRing.EtaMixin [definition, in ssralg]
GRing.UnitRing.inv [projection, in ssralg]
GRing.UnitRing.mixin [projection, in ssralg]
GRing.UnitRing.Mixin [constructor, in ssralg]
GRing.UnitRing.mixin_of [record, in ssralg]
GRing.UnitRing.pack [definition, in ssralg]
GRing.UnitRing.Pack [constructor, in ssralg]
GRing.UnitRing.ringType [definition, in ssralg]
GRing.UnitRing.sort [projection, in ssralg]
GRing.UnitRing.type [record, in ssralg]
GRing.UnitRing.unit [projection, in ssralg]
GRing.UnitRing.zmodType [definition, in ssralg]
GRing.unitrP [lemma, in ssralg]
GRing.unitr0 [lemma, in ssralg]
GRing.unitr1 [lemma, in ssralg]
GRing.unitr_exp [lemma, in ssralg]
GRing.unitr_inv [lemma, in ssralg]
GRing.unitr_mul [lemma, in ssralg]
GRing.unitr_mull [lemma, in ssralg]
GRing.unitr_mulr [lemma, in ssralg]
GRing.unitr_opp [lemma, in ssralg]
GRing.unitr_pexp [lemma, in ssralg]
GRing.Var [constructor, in ssralg]
GRing.wf_proj [lemma, in ssralg]
GRing.zero [definition, in ssralg]
GRing.ZmoduleTheory [section, in ssralg]
GRing.ZmoduleTheory.M [variable, in ssralg]
GRing.Zmodule.add [projection, in ssralg]
GRing.Zmodule.base [projection, in ssralg]
GRing.Zmodule.choiceType [definition, in ssralg]
GRing.Zmodule.Class [constructor, in ssralg]
GRing.Zmodule.class [definition, in ssralg]
GRing.Zmodule.class_of [record, in ssralg]
GRing.Zmodule.clone [definition, in ssralg]
GRing.Zmodule.eqType [definition, in ssralg]
GRing.Zmodule.ext [projection, in ssralg]
GRing.Zmodule.Mixin [constructor, in ssralg]
GRing.Zmodule.mixin_of [record, in ssralg]
GRing.Zmodule.opp [projection, in ssralg]
GRing.Zmodule.Pack [constructor, in ssralg]
GRing.Zmodule.pack [definition, in ssralg]
GRing.Zmodule.sort [projection, in ssralg]
GRing.Zmodule.type [record, in ssralg]
GRing.Zmodule.zero [projection, in ssralg]
gtn [definition, in ssrnat]
gtnNdvd [lemma, in div]
GtnNotLeq [constructor, in ssrnat]

---

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(5434 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(89 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(58 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(2752 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(233 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(145 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(139 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(50 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1267 entries)

Moduleid Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(47 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(24 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(609 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(21 entries)

---

Index

---

This page has been generated by coqdoc