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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 entries) |

Module 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |

## L

LaGrange [lemma, in groups]LaGrange [section, in groups]

LaGrangeI [lemma, in groups]

LaGrange.gT [variable, in groups]

LaGrange_index [lemma, in groups]

last [definition, in seq]

lastI [lemma, in seq]

LastNil [constructor, in seq]

lastP [lemma, in seq]

LastRcons [constructor, in seq]

last_cat [lemma, in seq]

last_cons [lemma, in seq]

last_ind [lemma, in seq]

last_map [lemma, in seq]

last_nth [lemma, in seq]

last_rcons [lemma, in seq]

last_spec [inductive, in seq]

last_traject [lemma, in paths]

lcmn [definition, in div]

lcmnA [lemma, in div]

lcmnC [lemma, in div]

lcmn0 [lemma, in div]

lcmn1 [lemma, in div]

lcmn_addoid [definition, in bigops]

lcmn_comoid [definition, in bigops]

lcmn_gt0 [lemma, in div]

lcmn_monoid [definition, in bigops]

lcm0n [lemma, in div]

lcm1n [lemma, in div]

lcoset [definition, in groups]

lcosetE [lemma, in groups]

lcosetM [lemma, in groups]

lcosetP [lemma, in groups]

lcosets [definition, in groups]

lcosetsP [lemma, in groups]

lcosets_invg [lemma, in groups]

lcoset_id [lemma, in groups]

lcoset_refl [lemma, in groups]

lcoset_sym [lemma, in groups]

lcoset_trans [lemma, in groups]

lcoset_transl [lemma, in groups]

lcoset_transr [lemma, in groups]

lcutmx [definition, in matrix]

lead_coef [definition, in poly]

lead_coefC [lemma, in poly]

lead_coefE [lemma, in poly]

lead_coefX [lemma, in poly]

lead_coefXn [lemma, in poly]

lead_coef0 [lemma, in poly]

lead_coef1 [lemma, in poly]

lead_coef_addl [lemma, in poly]

lead_coef_eq0 [lemma, in poly]

lead_coef_monic_mul [lemma, in poly]

lead_coef_mulX [lemma, in poly]

lead_coef_mul_id [lemma, in poly]

lead_coef_mul_monic [lemma, in poly]

lead_coef_opp [lemma, in poly]

lead_coef_poly [lemma, in poly]

lead_coef_proper_mul [lemma, in poly]

left_arc [lemma, in paths]

left_commutative [definition, in ssrfun]

left_distributive [definition, in ssrfun]

left_id [definition, in ssrfun]

left_inverse [definition, in ssrfun]

left_transitive [definition, in ssrbool]

left_zero [definition, in ssrfun]

leP [lemma, in ssrnat]

leq [definition, in ssrnat]

leqif [definition, in ssrnat]

leqifP [lemma, in ssrnat]

leqif_add [lemma, in ssrnat]

leqif_eq [lemma, in ssrnat]

leqif_geq [lemma, in ssrnat]

leqif_mul [lemma, in ssrnat]

leqif_refl [lemma, in ssrnat]

leqif_trans [lemma, in ssrnat]

leqNgt [lemma, in ssrnat]

leqnn [lemma, in ssrnat]

LeqNotGtn [constructor, in ssrnat]

leqnSn [lemma, in ssrnat]

leqn0 [lemma, in ssrnat]

leqP [lemma, in ssrnat]

leqSpred [lemma, in ssrnat]

leqW [lemma, in ssrnat]

leq0n [lemma, in ssrnat]

leq_add [lemma, in ssrnat]

leq_addl [lemma, in ssrnat]

leq_addr [lemma, in ssrnat]

leq_add2l [lemma, in ssrnat]

leq_add2r [lemma, in ssrnat]

leq_bigmax [lemma, in bigops]

leq_bigmax_cond [lemma, in bigops]

leq_b1 [lemma, in ssrnat]

leq_card_cover [lemma, in finset]

leq_card_setU [lemma, in finset]

leq_coef_size [lemma, in poly]

leq_div [lemma, in div]

leq_divl [lemma, in div]

leq_divr [lemma, in div]

leq_double [lemma, in ssrnat]

leq_eqVlt [lemma, in ssrnat]

leq_exp2l [lemma, in ssrnat]

leq_exp2r [lemma, in ssrnat]

leq_floor [lemma, in div]

leq_image_card [lemma, in fintype]

leq_imset_card [lemma, in finset]

leq_ltn_trans [lemma, in ssrnat]

leq_maxl [lemma, in ssrnat]

leq_maxr [lemma, in ssrnat]

leq_minl [lemma, in ssrnat]

leq_minr [lemma, in ssrnat]

leq_mod [lemma, in div]

leq_mul [lemma, in ssrnat]

leq_mul2l [lemma, in ssrnat]

leq_mul2r [lemma, in ssrnat]

leq_of_leqif [definition, in ssrnat]

leq_ord [lemma, in fintype]

leq_pdiv [lemma, in prime]

leq_pexp2l [lemma, in ssrnat]

leq_pmull [lemma, in ssrnat]

leq_pmulr [lemma, in ssrnat]

leq_pmul2l [lemma, in ssrnat]

leq_pmul2r [lemma, in ssrnat]

leq_pred [lemma, in ssrnat]

leq_Sdouble [lemma, in ssrnat]

leq_size_coef [lemma, in poly]

leq_size_perm [lemma, in seq]

leq_size_uniq [lemma, in seq]

leq_sqr [lemma, in ssrnat]

leq_subr [lemma, in ssrnat]

leq_subS [lemma, in ssrnat]

leq_sub2 [lemma, in ssrnat]

leq_sub2l [lemma, in ssrnat]

leq_sub2r [lemma, in ssrnat]

leq_sub_add [lemma, in ssrnat]

leq_total [lemma, in ssrnat]

leq_trans [lemma, in ssrnat]

leq_xor_gtn [inductive, in ssrnat]

le_irrelevance [lemma, in ssrnat]

lift [definition, in fintype]

liftK [lemma, in fintype]

lift0_mx [definition, in matrix]

lift0_mx_is_perm [lemma, in matrix]

lift0_mx_perm [lemma, in matrix]

lift0_perm [definition, in matrix]

lift0_permK [lemma, in matrix]

lift0_perm0 [lemma, in matrix]

lift0_perm_eq0 [lemma, in matrix]

lift0_perm_lift [lemma, in matrix]

lift_inj [lemma, in fintype]

lift_perm [definition, in matrix]

lift_permK [lemma, in matrix]

lift_permM [lemma, in matrix]

lift_permV [lemma, in matrix]

lift_perm1 [lemma, in matrix]

lift_perm_fun [definition, in matrix]

lift_perm_id [lemma, in matrix]

lift_perm_lift [lemma, in matrix]

lift_subproof [lemma, in fintype]

llsubmx [definition, in matrix]

LocalGlobal [section, in ssrbool]

LocalGlobal.d1 [variable, in ssrbool]

LocalGlobal.D1 [variable, in ssrbool]

LocalGlobal.d1' [variable, in ssrbool]

LocalGlobal.d2 [variable, in ssrbool]

LocalGlobal.D2 [variable, in ssrbool]

LocalGlobal.d2' [variable, in ssrbool]

LocalGlobal.D3 [variable, in ssrbool]

LocalGlobal.d3 [variable, in ssrbool]

LocalGlobal.d3' [variable, in ssrbool]

LocalGlobal.f [variable, in ssrbool]

LocalGlobal.f' [variable, in ssrbool]

LocalGlobal.g [variable, in ssrbool]

LocalGlobal.h [variable, in ssrbool]

LocalGlobal.P1 [variable, in ssrbool]

LocalGlobal.P2 [variable, in ssrbool]

LocalGlobal.P3 [variable, in ssrbool]

LocalGlobal.Q1 [variable, in ssrbool]

LocalGlobal.Q1l [variable, in ssrbool]

LocalGlobal.Q2 [variable, in ssrbool]

LocalGlobal.sub1 [variable, in ssrbool]

LocalGlobal.sub2 [variable, in ssrbool]

LocalGlobal.sub3 [variable, in ssrbool]

LocalGlobal.T1 [variable, in ssrbool]

LocalGlobal.T2 [variable, in ssrbool]

LocalGlobal.T3 [variable, in ssrbool]

LocalProperties [section, in ssrbool]

LocalProperties.d1 [variable, in ssrbool]

LocalProperties.d2 [variable, in ssrbool]

LocalProperties.d3 [variable, in ssrbool]

LocalProperties.f [variable, in ssrbool]

LocalProperties.T1 [variable, in ssrbool]

LocalProperties.T2 [variable, in ssrbool]

LocalProperties.T3 [variable, in ssrbool]

lock [lemma, in ssreflect]

locked [definition, in ssreflect]

logn [definition, in prime]

lognE [lemma, in prime]

logn0 [lemma, in prime]

logn1 [lemma, in prime]

logn_exp [lemma, in prime]

logn_gauss [lemma, in prime]

logn_gt0 [lemma, in prime]

logn_mul [lemma, in prime]

logn_prime [lemma, in prime]

logn_rec [definition, in prime]

lone_subgroup_char [lemma, in automorphism]

looping [definition, in paths]

loopingP [lemma, in paths]

looping_order [lemma, in connect]

looping_uniq [lemma, in paths]

lrsubmx [definition, in matrix]

lshift [definition, in fintype]

lshift_ord1 [lemma, in zmodp]

lshift_subproof [lemma, in fintype]

ltn [definition, in ssrnat]

ltngtP [lemma, in ssrnat]

ltnn [lemma, in ssrnat]

ltnNge [lemma, in ssrnat]

LtnNotGeq [constructor, in ssrnat]

ltnP [lemma, in ssrnat]

ltnS [lemma, in ssrnat]

ltnSn [lemma, in ssrnat]

ltnW [lemma, in ssrnat]

ltn0 [lemma, in ssrnat]

ltn0Sn [lemma, in ssrnat]

ltn_addl [lemma, in ssrnat]

ltn_addr [lemma, in ssrnat]

ltn_add2l [lemma, in ssrnat]

ltn_add2r [lemma, in ssrnat]

ltn_add_sub [lemma, in ssrnat]

ltn_ceil [lemma, in div]

ltn_divl [lemma, in div]

ltn_divr [lemma, in div]

ltn_double [lemma, in ssrnat]

ltn_expl [lemma, in ssrnat]

ltn_exp2l [lemma, in ssrnat]

ltn_exp2r [lemma, in ssrnat]

ltn_log0 [lemma, in prime]

ltn_mod [lemma, in div]

ltn_mul [lemma, in ssrnat]

ltn_mul2l [lemma, in ssrnat]

ltn_mul2r [lemma, in ssrnat]

ltn_neqAle [lemma, in ssrnat]

ltn_ord [lemma, in fintype]

ltn_Pdiv [lemma, in div]

ltn_pdiv2_prime [lemma, in prime]

ltn_pexp2l [lemma, in ssrnat]

ltn_pmod [lemma, in div]

ltn_Pmull [lemma, in ssrnat]

ltn_Pmulr [lemma, in ssrnat]

ltn_pmul2l [lemma, in ssrnat]

ltn_pmul2r [lemma, in ssrnat]

ltn_predK [lemma, in ssrnat]

ltn_Sdouble [lemma, in ssrnat]

ltn_size_undup [lemma, in seq]

ltn_sqr [lemma, in ssrnat]

ltn_subS [lemma, in ssrnat]

ltn_sub2l [lemma, in ssrnat]

ltn_sub2r [lemma, in ssrnat]

ltn_trans [lemma, in ssrnat]

ltn_unsplit [lemma, in fintype]

ltn_xor_geq [inductive, in ssrnat]

ltP [lemma, in ssrnat]

lt0n [lemma, in ssrnat]

lt0n_neq0 [lemma, in ssrnat]

lt0p [definition, in zmodp]

lt1p [definition, in zmodp]

lt_irrelevance [lemma, 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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 entries) |

Module 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |