CoCalc -- nolints.txt

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".
Project: Xena
Path: Maths_Challenges / _target / deps / mathlib / scripts / nolints.txt
Views: ¹⁸⁵³⁶
License: APACHE
1
import .all
2
run_cmd tactic.skip
3
apply_nolint
4
AddCommGroup
5
AddCommGroup.of
6
AddCommMon
7
AddCommMon.of
8
AddGroup
9
AddGroup.of
10
AddMon
11
AddMon.of
12
Cauchy.extend
13
Cauchy.gen
14
Class
15
CommRing.colimits.cocone_fun
16
CommRing.colimits.cocone_morphism
17
CommRing.colimits.colimit
18
CommRing.colimits.colimit_cocone
19
CommRing.colimits.colimit_is_colimit
20
CommRing.colimits.colimit_type
21
CommRing.colimits.desc_fun
22
CommRing.colimits.desc_fun_lift
23
CommRing.colimits.desc_morphism
24
CommRing.colimits.prequotient
25
CommRing.colimits.relation
26
CpltSepUniformSpace.to_UniformSpace
27
Gromov_Hausdorff.candidates_b_dist
28
Meas
29
Module.of
30
Mon.colimits.cocone_fun
31
Mon.colimits.cocone_morphism
32
Mon.colimits.colimit
33
Mon.colimits.colimit_cocone
34
Mon.colimits.colimit_is_colimit
35
Mon.colimits.colimit_type
36
Mon.colimits.desc_fun
37
Mon.colimits.desc_fun_lift
38
Mon.colimits.desc_morphism
39
Mon.colimits.prequotient
40
Mon.colimits.relation
41
Set.map_definable_aux
42
Set.mem
43
Set.mk
44
Set.subset
45
Top.colimit
46
Top.colimit_is_colimit
47
Top.limit
48
Top.limit_is_limit
49
Top.presheaf
50
Top.presheaf.pushforward
51
Top.presheaf.pushforward.comp
52
Top.presheaf.pushforward.id
53
Top.presheaf.pushforward_eq
54
Top.presheaf.stalk_pushforward
55
Well_order
56
abelianization
57
abelianization.lift
58
abelianization.lift.unique
59
abelianization.of
60
abv_sum_le_sum_abv
61
add_comm_group.is_Z_bilin
62
add_con.to_setoid
63
add_equiv.mk'
64
add_equiv.refl
65
add_equiv.symm
66
add_equiv.to_add_monoid_hom
67
add_equiv.to_equiv
68
add_equiv.trans
69
add_group.closure
70
add_group.in_closure
71
add_monoid.smul
72
add_monoid_hom.add
73
add_monoid_hom.comp
74
add_monoid_hom.id
75
add_monoid_hom.mk'
76
add_monoid_hom.neg
77
add_monoid_hom.zero
78
additive
79
adjoin_root
80
adjoin_root.lift
81
adjoin_root.mk
82
adjoin_root.of
83
adjoin_root.root
84
alg_hom.comp
85
alg_hom.id
86
alg_hom.range
87
alg_hom.to_ring_hom
88
algebra.adjoin
89
algebra.adjoin_eq_range
90
algebra.adjoin_singleton_eq_range
91
algebra.comap.comm_ring
92
algebra.comap.has_scalar
93
algebra.comap.of_comap
94
algebra.comap.ring
95
algebra.comap.to_comap
96
algebra.gi
97
algebra.lmul_left
98
algebra.lmul_right
99
algebra.of_id
100
algebra.to_comap
101
algebra.to_top
102
algebra_map
103
algebraic_geometry.PresheafedSpace.comp
104
algebraic_geometry.PresheafedSpace.id
105
algebraic_geometry.PresheafedSpace.stalk
106
algebraic_geometry.PresheafedSpace.stalk_map
107
alist.disjoint
108
alist.foldl
109
applicative_transformation
110
apply_fun_name
111
archimedean
112
archimedean.floor_ring
113
associated
114
associated.setoid
115
associates
116
associates.factor_set
117
associates.factor_set.coe_add
118
associates.factor_set.prod
119
associates.factors
120
associates.factors'
121
associates.mk
122
associates.out
123
associates.prime
124
associates.unique'
125
associates_int_equiv_nat
126
auto.add_conjuncts
127
auto.add_simps
128
auto.auto_config
129
auto.case_hyp
130
auto.case_option
131
auto.case_some_hyp
132
auto.case_some_hyp_aux
133
auto.classical_normalize_lemma_names
134
auto.common_normalize_lemma_names
135
auto.do_subst
136
auto.do_substs
137
auto.eelim
138
auto.eelims
139
auto.mk_hinst_lemmas
140
auto.normalize_hyp
141
auto.normalize_hyps
142
auto.normalize_negations
143
auto.preprocess_goal
144
auto.preprocess_hyps
145
auto.split_hyp
146
auto.split_hyps
147
auto.split_hyps_aux
148
auto.whnf_reducible
149
auto_cases_at
150
bicompl.bitraverse
151
bicompr.bitraverse
152
bifunctor
153
bifunctor.fst
154
bifunctor.snd
155
bilin_form.bilin_linear_map_equiv
156
bilin_form.to_linear_map
157
binder_eq_elim
158
binder_eq_elim.check
159
binder_eq_elim.check_eq
160
binder_eq_elim.old_conv
161
binder_eq_elim.pull
162
binder_eq_elim.push
163
bisequence
164
bitraversable
165
bounded_continuous_function.arzela_ascoli
166
bounded_continuous_function.arzela_ascoli₁
167
bounded_continuous_function.arzela_ascoli₂
168
bounded_continuous_function.const
169
bounded_continuous_function.dist_eq
170
bounded_continuous_function.dist_set_exists
171
bounded_continuous_function.equicontinuous_of_continuity_modulus
172
buffer.list_equiv_buffer
173
can_lift_attr
174
canonically_ordered_comm_semiring
175
card_subgroup_dvd_card
176
card_trivial
177
cardinal.aleph'.order_iso
178
cardinal.aleph_idx.initial_seg
179
cardinal.aleph_idx.order_iso
180
cardinal.cantor_function
181
cardinal.cantor_function_aux
182
cardinal.ord.order_embedding
183
cast_num
184
cast_pos_num
185
cast_znum
186
category_theory.Aut
187
category_theory.Kleisli
188
category_theory.Kleisli.comp_def
189
category_theory.Kleisli.id_def
190
category_theory.Kleisli.mk
191
category_theory.adjunction.adjunction_of_equiv_left
192
category_theory.adjunction.adjunction_of_equiv_right
193
category_theory.adjunction.cocones_iso
194
category_theory.adjunction.comp
195
category_theory.adjunction.cones_iso
196
category_theory.adjunction.core_hom_equiv
197
category_theory.adjunction.core_unit_counit
198
category_theory.adjunction.functoriality_counit
199
category_theory.adjunction.functoriality_counit'
200
category_theory.adjunction.functoriality_is_left_adjoint
201
category_theory.adjunction.functoriality_is_right_adjoint
202
category_theory.adjunction.functoriality_left_adjoint
203
category_theory.adjunction.functoriality_right_adjoint
204
category_theory.adjunction.functoriality_unit
205
category_theory.adjunction.functoriality_unit'
206
category_theory.adjunction.has_colimit_of_comp_equivalence
207
category_theory.adjunction.has_limit_of_comp_equivalence
208
category_theory.adjunction.id
209
category_theory.adjunction.left_adjoint_of_equiv
210
category_theory.adjunction.mk_of_hom_equiv
211
category_theory.adjunction.mk_of_unit_counit
212
category_theory.adjunction.right_adjoint_of_equiv
213
category_theory.as_iso
214
category_theory.category_struct
215
category_theory.comma
216
category_theory.comma.fst
217
category_theory.comma.map_left
218
category_theory.comma.map_left_comp
219
category_theory.comma.map_left_id
220
category_theory.comma.map_right
221
category_theory.comma.map_right_comp
222
category_theory.comma.map_right_id
223
category_theory.comma.nat_trans
224
category_theory.comma.snd
225
category_theory.comma_morphism
226
category_theory.core
227
category_theory.core.forget_functor_to_core
228
category_theory.core.inclusion
229
category_theory.coyoneda
230
category_theory.coyoneda.is_iso
231
category_theory.curry
232
category_theory.curry_obj
233
category_theory.currying
234
category_theory.discrete
235
category_theory.discrete.lift
236
category_theory.discrete.opposite
237
category_theory.epi
238
category_theory.eq_to_hom
239
category_theory.eq_to_iso
240
category_theory.equivalence.adjointify_η
241
category_theory.equivalence.counit
242
category_theory.equivalence.counit_inv
243
category_theory.equivalence.equivalence_of_fully_faithfully_ess_surj
244
category_theory.equivalence.ess_surj_of_equivalence
245
category_theory.equivalence.fun_inv_id_assoc
246
category_theory.equivalence.inv_fun_id_assoc
247
category_theory.equivalence.mk
248
category_theory.equivalence.refl
249
category_theory.equivalence.symm
250
category_theory.equivalence.to_adjunction
251
category_theory.equivalence.trans
252
category_theory.equivalence.unit
253
category_theory.equivalence.unit_inv
254
category_theory.ess_surj
255
category_theory.ess_surj.iso
256
category_theory.evaluation
257
category_theory.evaluation_uncurried
258
category_theory.full_subcategory_inclusion
259
category_theory.functor.adjunction
260
category_theory.functor.as_equivalence
261
category_theory.functor.associator
262
category_theory.functor.const
263
category_theory.functor.const.op_obj_op
264
category_theory.functor.const.op_obj_unop
265
category_theory.functor.flip
266
category_theory.functor.fun_inv_id
267
category_theory.functor.fun_obj_preimage_iso
268
category_theory.functor.inv
269
category_theory.functor.inv_fun_id
270
category_theory.functor.left_op
271
category_theory.functor.left_unitor
272
category_theory.functor.map_cocone_morphism
273
category_theory.functor.map_cone_inv
274
category_theory.functor.map_cone_morphism
275
category_theory.functor.map_iso
276
category_theory.functor.obj_preimage
277
category_theory.functor.of_function
278
category_theory.functor.op
279
category_theory.functor.op_hom
280
category_theory.functor.op_inv
281
category_theory.functor.right_op
282
category_theory.functor.right_unitor
283
category_theory.functor.sections
284
category_theory.functor.star
285
category_theory.functor.to_cocone
286
category_theory.functor.to_cone
287
category_theory.functor.ulift_down
288
category_theory.functor.ulift_down_up
289
category_theory.functor.ulift_up
290
category_theory.functor.ulift_up_down
291
category_theory.functor.unop
292
category_theory.has_hom
293
category_theory.has_hom.hom.op
294
category_theory.has_hom.hom.unop
295
category_theory.has_limits_of_reflective
296
category_theory.hom_of_element
297
category_theory.induced_category
298
category_theory.induced_functor
299
category_theory.is_equivalence.mk
300
category_theory.is_iso_of_fully_faithful
301
category_theory.is_iso_of_op
302
category_theory.is_left_adjoint
303
category_theory.is_right_adjoint
304
category_theory.iso
305
category_theory.iso.hom_congr
306
category_theory.iso.op
307
category_theory.iso.refl
308
category_theory.iso.symm
309
category_theory.iso.to_equiv
310
category_theory.iso.trans
311
category_theory.iso_whisker_left
312
category_theory.iso_whisker_right
313
category_theory.large_groupoid
314
category_theory.left_adjoint
315
category_theory.limits.binary_cofan
316
category_theory.limits.binary_cofan.mk
317
category_theory.limits.binary_fan
318
category_theory.limits.binary_fan.mk
319
category_theory.limits.cocone.equiv
320
category_theory.limits.cocone.extensions
321
category_theory.limits.cocone.of_cofork
322
category_theory.limits.cocone.of_pushout_cocone
323
category_theory.limits.cocone.whisker
324
category_theory.limits.cocone_left_op_of_cone
325
category_theory.limits.cocone_morphism
326
category_theory.limits.cocone_of_cone_left_op
327
category_theory.limits.cocones.forget
328
category_theory.limits.cocones.functoriality
329
category_theory.limits.cocones.precompose
330
category_theory.limits.cocones.precompose_comp
331
category_theory.limits.cocones.precompose_equivalence
332
category_theory.limits.cocones.precompose_id
333
category_theory.limits.coequalizer
334
category_theory.limits.coequalizer.desc
335
category_theory.limits.coequalizer.π
336
category_theory.limits.cofan
337
category_theory.limits.cofan.mk
338
category_theory.limits.cofork
339
category_theory.limits.cofork.of_cocone
340
category_theory.limits.cofork.of_π
341
category_theory.limits.cofork.π
342
category_theory.limits.colim_coyoneda
343
category_theory.limits.colimit
344
category_theory.limits.colimit.cocone
345
category_theory.limits.colimit.cocone_morphism
346
category_theory.limits.colimit.desc
347
category_theory.limits.colimit.hom_iso
348
category_theory.limits.colimit.hom_iso'
349
category_theory.limits.colimit.is_colimit
350
category_theory.limits.colimit.post
351
category_theory.limits.colimit.pre
352
category_theory.limits.colimit.ι
353
category_theory.limits.cone.equiv
354
category_theory.limits.cone.extensions
355
category_theory.limits.cone.of_fork
356
category_theory.limits.cone.of_pullback_cone
357
category_theory.limits.cone.whisker
358
category_theory.limits.cone_left_op_of_cocone
359
category_theory.limits.cone_morphism
360
category_theory.limits.cone_of_cocone_left_op
361
category_theory.limits.cones.forget
362
category_theory.limits.cones.functoriality
363
category_theory.limits.cones.postcompose
364
category_theory.limits.cones.postcompose_comp
365
category_theory.limits.cones.postcompose_equivalence
366
category_theory.limits.cones.postcompose_id
367
category_theory.limits.coprod
368
category_theory.limits.coprod.desc
369
category_theory.limits.coprod.inl
370
category_theory.limits.coprod.inr
371
category_theory.limits.coprod.map
372
category_theory.limits.equalizer
373
category_theory.limits.equalizer.lift
374
category_theory.limits.equalizer.ι
375
category_theory.limits.evaluate_functor_category_colimit_cocone
376
category_theory.limits.evaluate_functor_category_limit_cone
377
category_theory.limits.fan
378
category_theory.limits.fan.mk
379
category_theory.limits.fork
380
category_theory.limits.fork.of_cone
381
category_theory.limits.fork.of_ι
382
category_theory.limits.fork.ι
383
category_theory.limits.functor_category_colimit_cocone
384
category_theory.limits.functor_category_is_colimit_cocone
385
category_theory.limits.functor_category_is_limit_cone
386
category_theory.limits.functor_category_limit_cone
387
category_theory.limits.has_binary_coproducts
388
category_theory.limits.has_binary_products
389
category_theory.limits.has_coequalizers
390
category_theory.limits.has_colimit_of_equivalence_comp
391
category_theory.limits.has_colimit_of_iso
392
category_theory.limits.has_colimits_of_shape_of_equivalence
393
category_theory.limits.has_coproducts
394
category_theory.limits.has_equalizers
395
category_theory.limits.has_finite_colimits
396
category_theory.limits.has_finite_coproducts
397
category_theory.limits.has_finite_limits
398
category_theory.limits.has_finite_products
399
category_theory.limits.has_initial
400
category_theory.limits.has_limit_of_equivalence_comp
401
category_theory.limits.has_limit_of_iso
402
category_theory.limits.has_limits_of_shape_of_equivalence
403
category_theory.limits.has_products
404
category_theory.limits.has_pullbacks
405
category_theory.limits.has_pushouts
406
category_theory.limits.has_terminal
407
category_theory.limits.initial
408
category_theory.limits.initial.to
409
category_theory.limits.is_colimit.desc_cocone_morphism
410
category_theory.limits.is_colimit.hom_iso'
411
category_theory.limits.is_colimit.iso_unique_cocone_morphism
412
category_theory.limits.is_colimit.mk_cocone_morphism
413
category_theory.limits.is_colimit.of_iso_colimit
414
category_theory.limits.is_limit.hom_iso'
415
category_theory.limits.is_limit.iso_unique_cone_morphism
416
category_theory.limits.is_limit.lift_cone_morphism
417
category_theory.limits.is_limit.mk_cone_morphism
418
category_theory.limits.is_limit.of_iso_limit
419
category_theory.limits.lim_yoneda
420
category_theory.limits.limit
421
category_theory.limits.limit.cone
422
category_theory.limits.limit.cone_morphism
423
category_theory.limits.limit.hom_iso
424
category_theory.limits.limit.hom_iso'
425
category_theory.limits.limit.is_limit
426
category_theory.limits.limit.lift
427
category_theory.limits.limit.post
428
category_theory.limits.limit.pre
429
category_theory.limits.limit.π
430
category_theory.limits.map_pair
431
category_theory.limits.pair
432
category_theory.limits.pair_function
433
category_theory.limits.parallel_pair
434
category_theory.limits.pi.lift
435
category_theory.limits.pi.map
436
category_theory.limits.pi.π
437
category_theory.limits.preserves_colimit
438
category_theory.limits.preserves_colimits
439
category_theory.limits.preserves_colimits_of_shape
440
category_theory.limits.preserves_limit
441
category_theory.limits.preserves_limits
442
category_theory.limits.preserves_limits_of_shape
443
category_theory.limits.prod
444
category_theory.limits.prod.fst
445
category_theory.limits.prod.lift
446
category_theory.limits.prod.map
447
category_theory.limits.prod.snd
448
category_theory.limits.pullback.fst
449
category_theory.limits.pullback.lift
450
category_theory.limits.pullback.snd
451
category_theory.limits.pullback_cone
452
category_theory.limits.pullback_cone.fst
453
category_theory.limits.pullback_cone.mk
454
category_theory.limits.pullback_cone.of_cone
455
category_theory.limits.pullback_cone.snd
456
category_theory.limits.pushout.desc
457
category_theory.limits.pushout.inl
458
category_theory.limits.pushout.inr
459
category_theory.limits.pushout_cocone
460
category_theory.limits.pushout_cocone.inl
461
category_theory.limits.pushout_cocone.inr
462
category_theory.limits.pushout_cocone.mk
463
category_theory.limits.pushout_cocone.of_cocone
464
category_theory.limits.reflects_colimit
465
category_theory.limits.reflects_colimits
466
category_theory.limits.reflects_colimits_of_shape
467
category_theory.limits.reflects_limit
468
category_theory.limits.reflects_limits
469
category_theory.limits.reflects_limits_of_shape
470
category_theory.limits.sigma.desc
471
category_theory.limits.sigma.map
472
category_theory.limits.sigma.ι
473
category_theory.limits.terminal
474
category_theory.limits.terminal.from
475
category_theory.limits.types.colimit
476
category_theory.limits.types.colimit_is_colimit
477
category_theory.limits.types.limit
478
category_theory.limits.types.limit_is_limit
479
category_theory.limits.types.types_colimit_pre
480
category_theory.limits.walking_cospan.hom.comp
481
category_theory.limits.walking_parallel_pair_hom.comp
482
category_theory.limits.walking_span.hom.comp
483
category_theory.monad
484
category_theory.monad.algebra.hom
485
category_theory.monad.algebra.hom.comp
486
category_theory.monad.algebra.hom.id
487
category_theory.monad.comparison
488
category_theory.monad.comparison_forget
489
category_theory.monad.forget
490
category_theory.monad.forget_creates_limits
491
category_theory.monad.forget_creates_limits.c
492
category_theory.monad.forget_creates_limits.cone_point
493
category_theory.monad.forget_creates_limits.γ
494
category_theory.monad.free
495
category_theory.monadic_creates_limits
496
category_theory.mono
497
category_theory.monoidal_functor.ε_iso
498
category_theory.monoidal_functor.μ_iso
499
category_theory.nat_iso.hcomp
500
category_theory.nat_iso.is_iso_app_of_is_iso
501
category_theory.nat_iso.is_iso_of_is_iso_app
502
category_theory.nat_iso.of_components
503
category_theory.nat_iso.of_isos
504
category_theory.nat_iso.op
505
category_theory.nat_trans.left_op
506
category_theory.nat_trans.of_function
507
category_theory.nat_trans.of_homs
508
category_theory.nat_trans.on_presheaf
509
category_theory.nat_trans.op
510
category_theory.nat_trans.right_op
511
category_theory.nat_trans.unop
512
category_theory.obviously'
513
category_theory.op_op
514
category_theory.over
515
category_theory.over.colimit
516
category_theory.over.forget
517
category_theory.over.forget_colimit_is_colimit
518
category_theory.over.hom_mk
519
category_theory.over.map
520
category_theory.over.mk
521
category_theory.over.post
522
category_theory.prod.associativity
523
category_theory.prod.associator
524
category_theory.prod.braiding
525
category_theory.prod.inverse_associator
526
category_theory.prod.swap
527
category_theory.prod.symmetry
528
category_theory.representable
529
category_theory.right_adjoint
530
category_theory.single_obj
531
category_theory.single_obj.star
532
category_theory.small_groupoid
533
category_theory.sum.associativity
534
category_theory.sum.associator
535
category_theory.sum.inverse_associator
536
category_theory.ulift_functor
537
category_theory.ulift_trivial
538
category_theory.uncurry
539
category_theory.under
540
category_theory.under.forget
541
category_theory.under.forget_limit_is_limit
542
category_theory.under.hom_mk
543
category_theory.under.limit
544
category_theory.under.map
545
category_theory.under.mk
546
category_theory.under.post
547
category_theory.whisker_left
548
category_theory.whisker_right
549
category_theory.whiskering_left
550
category_theory.whiskering_right
551
category_theory.yoneda
552
category_theory.yoneda.is_iso
553
category_theory.yoneda_evaluation
554
category_theory.yoneda_lemma
555
category_theory.yoneda_pairing
556
category_theory.yoneda_sections
557
category_theory.yoneda_sections_small
558
cau_seq
559
cau_seq.abv_pos_of_not_lim_zero
560
cau_seq.bounded'
561
cau_seq.cauchy
562
cau_seq.cauchy₂
563
cau_seq.cauchy₃
564
cau_seq.completion.Cauchy
565
cau_seq.completion.discrete_field
566
cau_seq.completion.mk
567
cau_seq.completion.of_rat
568
cau_seq.equiv_def₃
569
cau_seq.inv
570
cau_seq.inv_aux
571
cau_seq.is_complete
572
cau_seq.le_of_exists
573
cau_seq.lim
574
cau_seq.lim_zero
575
cau_seq.of_eq
576
cau_seq.of_near
577
cauchy_product
578
cauchy_seq_bdd
579
centralizer.add_submonoid
580
cfilter.to_realizer
581
char_p.char_is_prime_of_ge_two
582
classical.DLO
583
classical.all_definable
584
classical.exists_cases
585
classical.inhabited_of_nonempty'
586
comm_ring.anti_equiv_to_equiv
587
comm_ring.equiv_to_anti_equiv
588
commutator
589
comp.seq
590
compact.realizer
591
completion
592
complex
593
complex.I
594
complex.abs
595
complex.cau_seq_abs
596
complex.cau_seq_conj
597
complex.cau_seq_im
598
complex.cau_seq_re
599
complex.conj
600
complex.cos
601
complex.cosh
602
complex.exp
603
complex.exp'
604
complex.lim_aux
605
complex.norm_sq
606
complex.of_real
607
complex.real_prod_equiv
608
complex.sin
609
complex.sinh
610
complex.tan
611
complex.tanh
612
computable
613
computable_pred
614
computable₂
615
computation.bind.F
616
computation.bind.G
617
computation.bisim_o
618
computation.cases_on
619
computation.corec.F
620
computation.is_bisimulation
621
computation.lift_rel_aux
622
computation.map_congr
623
computation.mem
624
computation.mem_rec_on
625
computation.parallel.aux1
626
computation.parallel.aux2
627
computation.parallel_rec
628
computation.terminates_rec_on
629
con.to_setoid
630
const.bitraverse
631
constr_smul
632
cont
633
cont_t
634
cont_t.map
635
cont_t.monad_lift
636
cont_t.run
637
cont_t.with_cont_t
638
continuous.comap
639
continuous_map
640
continuous_map.coev
641
continuous_map.compact_open.gen
642
continuous_map.ev
643
continuous_map.induced
644
continuous_of_locally_uniform_limit_of_continuous
645
continuous_of_uniform_limit_of_continuous
646
conv.discharge_eq_lhs
647
conv.interactive.erw
648
conv.interactive.norm_cast
649
conv.interactive.norm_num
650
conv.interactive.norm_num1
651
conv.interactive.ring
652
conv.interactive.ring2
653
conv.repeat_count
654
conv.repeat_with_results
655
conv.replace_lhs
656
conv.slice
657
conv.slice_lhs
658
conv.slice_rhs
659
ctop.realizer.id
660
ctop.realizer.nhds
661
ctop.realizer.nhds_F
662
ctop.realizer.nhds_σ
663
ctop.realizer.of_equiv
664
ctop.to_realizer
665
decidable.lt_by_cases
666
decidable_linear_order.lift
667
decidable_linear_order_of_is_well_order
668
decidable_of_bool
669
decidable_of_iff
670
decidable_of_iff'
671
decidable_zero_symm
672
declaration.update_with_fun
673
dense_or_discrete
674
denumerable.equiv₂
675
denumerable.eqv
676
denumerable.lower
677
denumerable.lower'
678
denumerable.mk'
679
denumerable.of_encodable_of_infinite
680
denumerable.of_equiv
681
denumerable.of_nat
682
denumerable.pair
683
denumerable.raise
684
denumerable.raise'
685
denumerable.raise'_finset
686
dfinsupp
687
dfinsupp.decidable_eq
688
dfinsupp.erase
689
dfinsupp.lmk
690
dfinsupp.lsingle
691
dfinsupp.map_range_def
692
dfinsupp.map_range_single
693
dfinsupp.mk
694
dfinsupp.pre
695
dfinsupp.single
696
dfinsupp.subtype_domain_sum
697
dfinsupp.sum_apply
698
dfinsupp.support
699
dfinsupp.to_has_scalar
700
dfinsupp.to_module
701
dfinsupp.zip_with
702
dfinsupp.zip_with_def
703
dioph.pell_dioph
704
dioph.xn_dioph
705
direct_sum
706
direct_sum.component
707
direct_sum.id
708
direct_sum.lid
709
direct_sum.lmk
710
direct_sum.lof
711
direct_sum.lset_to_set
712
direct_sum.mk
713
direct_sum.of
714
direct_sum.set_to_set
715
direct_sum.to_group
716
direct_sum.to_module
717
directed_order
718
dlist.join
719
dlist.list_equiv_dlist
720
eckmann_hilton.comm_group
721
eckmann_hilton.comm_monoid
722
eckmann_hilton.is_unital
723
emetric.cauchy_iff
724
emetric.cauchy_seq_iff
725
emetric.cauchy_seq_iff'
726
emetric.exists_ball_subset_ball
727
emetric.is_open_iff
728
emetric.mem_closure_iff'
729
emetric.mem_nhds_iff
730
emetric.nhds_eq
731
emetric.tendsto_at_top
732
emetric.tendsto_nhds
733
emetric.totally_bounded_iff
734
emetric.totally_bounded_iff'
735
emetric.uniform_continuous_iff
736
emetric.uniform_embedding_iff
737
emetric.uniform_embedding_iff'
738
empty.elim
739
enat
740
encodable.choose
741
encodable.choose_x
742
encodable.decidable_eq_of_encodable
743
encodable.decidable_range_encode
744
encodable.decode2
745
encodable.decode_list
746
encodable.decode_multiset
747
encodable.decode_sigma
748
encodable.decode_subtype
749
encodable.decode_sum
750
encodable.encodable_of_list
751
encodable.encode_list
752
encodable.encode_multiset
753
encodable.encode_sigma
754
encodable.encode_subtype
755
encodable.encode_sum
756
encodable.equiv_range_encode
757
encodable.fintype_arrow
758
encodable.fintype_pi
759
encodable.of_inj
760
encodable.of_left_injection
761
encodable.of_left_inverse
762
encodable.trunc_encodable_of_fintype
763
ennreal.Icc_mem_nhds
764
ennreal.ennreal_equiv_nnreal
765
ennreal.ennreal_equiv_sum
766
ennreal.nhds_of_ne_top
767
ennreal.tendsto_at_top
768
ennreal.tendsto_nhds
769
eq_of_forall_dist_le
770
eq_of_forall_edist_le
771
eq_of_le_of_forall_ge_of_dense
772
eq_of_le_of_forall_le_of_dense
773
equiv.Pi_congr_right
774
equiv.Pi_curry
775
equiv.Prop_equiv_bool
776
equiv.add_comm_group
777
equiv.add_comm_monoid
778
equiv.add_comm_semigroup
779
equiv.add_group
780
equiv.add_left
781
equiv.add_monoid
782
equiv.add_right
783
equiv.add_semigroup
784
equiv.array_equiv_fin
785
equiv.arrow_arrow_equiv_prod_arrow
786
equiv.arrow_congr
787
equiv.arrow_prod_equiv_prod_arrow
788
equiv.arrow_punit_equiv_punit
789
equiv.bool_equiv_punit_sum_punit
790
equiv.bool_prod_equiv_sum
791
equiv.bool_prod_nat_equiv_nat
792
equiv.cast
793
equiv.comm_group
794
equiv.comm_monoid
795
equiv.comm_ring
796
equiv.comm_semigroup
797
equiv.comm_semiring
798
equiv.conj
799
equiv.d_array_equiv_fin
800
equiv.decidable_eq
801
equiv.decidable_eq_of_equiv
802
equiv.discrete_field
803
equiv.division_ring
804
equiv.domain
805
equiv.empty_arrow_equiv_punit
806
equiv.empty_equiv_pempty
807
equiv.empty_of_not_nonempty
808
equiv.empty_prod
809
equiv.empty_sum
810
equiv.equiv_congr
811
equiv.equiv_empty
812
equiv.equiv_pempty
813
equiv.false_arrow_equiv_punit
814
equiv.false_equiv_empty
815
equiv.false_equiv_pempty
816
equiv.field
817
equiv.fin_equiv_subtype
818
equiv.functor
819
equiv.group
820
equiv.has_add
821
equiv.has_inv
822
equiv.has_mul
823
equiv.has_neg
824
equiv.has_one
825
equiv.has_zero
826
equiv.inhabited_of_equiv
827
equiv.int_equiv_nat
828
equiv.int_equiv_nat_sum_nat
829
equiv.integral_domain
830
equiv.inv
831
equiv.is_lawful_traversable
832
equiv.is_lawful_traversable'
833
equiv.list_equiv_of_equiv
834
equiv.list_equiv_self_of_equiv_nat
835
equiv.list_nat_equiv_nat
836
equiv.map
837
equiv.monoid
838
equiv.mul_left
839
equiv.mul_right
840
equiv.nat_equiv_nat_sum_punit
841
equiv.nat_prod_nat_equiv_nat
842
equiv.nat_sum_nat_equiv_nat
843
equiv.nat_sum_punit_equiv_nat
844
equiv.neg
845
equiv.nonzero_comm_ring
846
equiv.of_bijective
847
equiv.option_equiv_sum_punit
848
equiv.pempty_arrow_equiv_punit
849
equiv.pempty_equiv_pempty
850
equiv.pempty_of_not_nonempty
851
equiv.pempty_prod
852
equiv.pempty_sum
853
equiv.perm.card_support_swap
854
equiv.perm.cycle_factors
855
equiv.perm.cycle_factors_aux
856
equiv.perm.cycle_of
857
equiv.perm.disjoint
858
equiv.perm.eq_swap_of_is_cycle_of_apply_apply_eq_self
859
equiv.perm.is_cycle
860
equiv.perm.is_cycle_swap
861
equiv.perm.is_cycle_swap_mul_aux₁
862
equiv.perm.is_swap
863
equiv.perm.of_subtype
864
equiv.perm.same_cycle
865
equiv.perm.sign_aux
866
equiv.perm.sign_aux2
867
equiv.perm.sign_aux3
868
equiv.perm.sign_bij_aux
869
equiv.perm.sign_cycle
870
equiv.perm.subtype_perm
871
equiv.perm.support
872
equiv.perm.support_swap
873
equiv.perm.swap_factors_aux
874
equiv.perm.trunc_swap_factors
875
equiv.perm_congr
876
equiv.pi_equiv_subtype_sigma
877
equiv.plift
878
equiv.pnat_equiv_nat
879
equiv.prod_assoc
880
equiv.prod_comm
881
equiv.prod_congr
882
equiv.prod_empty
883
equiv.prod_equiv_of_equiv_nat
884
equiv.prod_pempty
885
equiv.prod_punit
886
equiv.prod_sum_distrib
887
equiv.prop_equiv_punit
888
equiv.psigma_equiv_sigma
889
equiv.psum_equiv_sum
890
equiv.punit_arrow_equiv
891
equiv.punit_equiv_punit
892
equiv.punit_prod
893
equiv.refl
894
equiv.ring
895
equiv.semigroup
896
equiv.semiring
897
equiv.set.congr
898
equiv.set.empty
899
equiv.set.image
900
equiv.set.image_of_inj_on
901
equiv.set.insert
902
equiv.set.of_eq
903
equiv.set.pempty
904
equiv.set.prod
905
equiv.set.range
906
equiv.set.sep
907
equiv.set.singleton
908
equiv.set.sum_compl
909
equiv.set.union
910
equiv.set.union'
911
equiv.set.union_sum_inter
912
equiv.set.univ
913
equiv.set_congr
914
equiv.sigma_congr_left
915
equiv.sigma_congr_right
916
equiv.sigma_equiv_prod
917
equiv.sigma_equiv_prod_of_equiv
918
equiv.sigma_preimage_equiv
919
equiv.sigma_prod_distrib
920
equiv.sigma_subtype_preimage_equiv
921
equiv.sigma_subtype_preimage_equiv_subtype
922
equiv.subtype_congr
923
equiv.subtype_congr_prop
924
equiv.subtype_congr_right
925
equiv.subtype_equiv_of_subtype'
926
equiv.subtype_pi_equiv_pi
927
equiv.subtype_quotient_equiv_quotient_subtype
928
equiv.subtype_subtype_equiv_subtype_exists
929
equiv.subtype_subtype_equiv_subtype_inter
930
equiv.sum_arrow_equiv_prod_arrow
931
equiv.sum_assoc
932
equiv.sum_comm
933
equiv.sum_congr
934
equiv.sum_empty
935
equiv.sum_equiv_sigma_bool
936
equiv.sum_pempty
937
equiv.sum_prod_distrib
938
equiv.swap_core
939
equiv.symm
940
equiv.to_embedding
941
equiv.to_iso
942
equiv.to_pequiv
943
equiv.trans
944
equiv.traversable
945
equiv.traverse
946
equiv.true_equiv_punit
947
equiv.ulift
948
equiv.unique_congr
949
equiv.unique_of_equiv
950
equiv.units_equiv_ne_zero
951
equiv.vector_equiv_array
952
equiv.vector_equiv_fin
953
equiv.zero_ne_one_class
954
equiv_of_dim_eq_dim
955
equiv_of_unique_of_unique
956
equiv_punit_of_unique
957
equiv_type_constr
958
erased.bind
959
erased.choice
960
erased.equiv
961
erased.join
962
erased.mk
963
erased.out
964
erased.out_type
965
euclidean_domain
966
euclidean_domain.gcd
967
euclidean_domain.lcm
968
euclidean_domain.xgcd_aux
969
except_t.call_cc
970
except_t.mk_label
971
except_t.pass_aux
972
exists.classical_rec_on
973
exists_eq_elim
974
exists_forall_ge_and
975
exists_gpow_eq_one
976
exists_mem_ne_zero_of_dim_pos
977
exists_pow_eq_one
978
expr.flip_eq
979
expr.flip_iff
980
expr.get_pis
981
ext_param
982
ext_param_type
983
field.closure
984
field.direct_limit.discrete_field
985
field.direct_limit.field
986
field.direct_limit.inv
987
filter
988
filter.Liminf
989
filter.Liminf_le_Liminf
990
filter.Liminf_le_Liminf_of_le
991
filter.Liminf_le_Limsup
992
filter.Liminf_le_of_le
993
filter.Limsup
994
filter.filter_product.abs_def
995
filter.filter_product.of_seq
996
filter.filter_product.of_seq_one
997
filter.filter_product.of_seq_zero
998
filter.gi_generate
999
filter.hyperfilter
1000
filter.infi_ne_bot_iff_of_directed
1001
filter.infi_ne_bot_iff_of_directed'
1002
filter.infi_ne_bot_of_directed
1003
filter.infi_ne_bot_of_directed'
1004
filter.infi_sets_eq
1005
filter.is_bounded_default
1006
filter.is_bounded_ge_of_bot
1007
filter.is_bounded_under
1008
filter.is_bounded_under_inf
1009
filter.is_cobounded_ge_of_top
1010
filter.is_cobounded_under
1011
filter.is_trans_ge
1012
filter.le_Liminf_of_le
1013
filter.lift_infi'
1014
filter.liminf
1015
filter.liminf_eq_supr_infi_of_nat
1016
filter.liminf_le_liminf
1017
filter.limsup
1018
filter.limsup_eq_infi_supr_of_nat
1019
filter.map_at_top_eq_of_gc
1020
filter.map_binfi_eq
1021
filter.map_div_at_top_eq_nat
1022
filter.map_infi_eq
1023
filter.mem_at_top_sets
1024
filter.mem_infi
1025
filter.mk_of_closure
1026
filter.monad
1027
filter.pcomap'
1028
filter.pmap
1029
filter.pointwise_add
1030
filter.pointwise_add_add_monoid
1031
filter.pointwise_mul
1032
filter.pointwise_mul_monoid
1033
filter.pointwise_one
1034
filter.pointwise_zero
1035
filter.ptendsto
1036
filter.ptendsto'
1037
filter.rcomap
1038
filter.rcomap'
1039
filter.realizer.of_eq
1040
filter.rmap
1041
filter.rtendsto
1042
filter.rtendsto'
1043
filter.tendsto_at_top'
1044
filter.tendsto_at_top_at_bot
1045
filter.tendsto_at_top_principal
1046
filter.ultrafilter.bind
1047
filter.ultrafilter.map
1048
filter.ultrafilter.pure
1049
fin.add_nat_val
1050
fin.cases
1051
fin.clamp
1052
fin.succ_rec
1053
fin.succ_rec_on
1054
fin2.cases'
1055
fin2.elim0
1056
fin_dim_vectorspace_equiv
1057
fin_one_equiv
1058
fin_prod_fin_equiv
1059
fin_two_equiv
1060
fin_zero_elim'
1061
fin_zero_equiv
1062
find_cmd
1063
finite_field.field_of_integral_domain
1064
finmap.all
1065
finmap.any
1066
finmap.disjoint
1067
finmap.foldl
1068
finmap.sdiff
1069
finset.attach_fin
1070
finset.choose
1071
finset.choose_x
1072
finset.empty
1073
finset.insert_none
1074
finset.map
1075
finset.map_embedding
1076
finset.max
1077
finset.max'
1078
finset.min
1079
finset.min'
1080
finset.pi
1081
finset.pi.cons
1082
finset.pi.empty
1083
finset.powerset_len
1084
finset.preimage
1085
finset.prod_ite
1086
finset.strong_induction_on
1087
finset.subtype
1088
finset.sum
1089
finset.sum_ite
1090
finsets
1091
finsupp.antidiagonal
1092
finsupp.comap_domain
1093
finsupp.congr
1094
finsupp.curry
1095
finsupp.dom_congr
1096
finsupp.dom_lcongr
1097
finsupp.equiv_fun_on_fintype
1098
finsupp.equiv_multiset
1099
finsupp.erase
1100
finsupp.finsupp_prod_equiv
1101
finsupp.frange
1102
finsupp.lapply
1103
finsupp.lmap_domain
1104
finsupp.lsingle
1105
finsupp.lsubtype_domain
1106
finsupp.lsum
1107
finsupp.of_multiset
1108
finsupp.restrict_dom
1109
finsupp.restrict_support_equiv
1110
finsupp.split
1111
finsupp.split_comp
1112
finsupp.split_support
1113
finsupp.supported
1114
finsupp.supported_eq_span_single
1115
finsupp.supported_equiv_finsupp
1116
finsupp.to_multiset
1117
finsupp.total_on
1118
finsupp.uncurry
1119
fintype.bij_inv
1120
fintype.choose
1121
fintype.choose_x
1122
fintype.fintype_prod_left
1123
fintype.fintype_prod_right
1124
fintype.of_injective
1125
fintype.of_subsingleton
1126
fintype.subtype
1127
fintype_perm
1128
flip.bitraverse
1129
forall_eq_elim
1130
forall_ge_le_of_forall_le_succ
1131
fp.div_nat_lt_two_pow
1132
fp.emax
1133
fp.emin
1134
fp.float
1135
fp.float.add
1136
fp.float.div
1137
fp.float.is_finite
1138
fp.float.is_zero
1139
fp.float.mul
1140
fp.float.neg
1141
fp.float.sign
1142
fp.float.sign'
1143
fp.float.sub
1144
fp.float.zero
1145
fp.float_cfg
1146
fp.next_dn
1147
fp.next_dn_pos
1148
fp.next_up
1149
fp.next_up_pos
1150
fp.of_pos_rat_dn
1151
fp.of_rat
1152
fp.of_rat_dn
1153
fp.of_rat_up
1154
fp.prec
1155
fp.rmode
1156
fp.to_rat
1157
fp.valid_finite
1158
free_abelian_group
1159
free_abelian_group.lift
1160
free_abelian_group.lift.universal
1161
free_abelian_group.of
1162
free_add_monoid
1163
free_comm_ring
1164
free_comm_ring.is_supported
1165
free_comm_ring.lift
1166
free_comm_ring.map
1167
free_comm_ring.of
1168
free_comm_ring.restriction
1169
free_comm_ring_equiv_mv_polynomial_int
1170
free_comm_ring_pempty_equiv_int
1171
free_comm_ring_punit_equiv_polynomial_int
1172
free_group.free_group_empty_equiv_unit
1173
free_group.free_group_unit_equiv_int
1174
free_group.map.aux
1175
free_group.mk
1176
free_group.to_group.aux
1177
free_magma
1178
free_magma.length
1179
free_magma.lift
1180
free_magma.map
1181
free_magma.repr'
1182
free_magma.traverse
1183
free_monoid
1184
free_ring
1185
free_ring.lift
1186
free_ring.map
1187
free_ring.of
1188
free_ring.subsingleton_equiv_free_comm_ring
1189
free_ring.to_free_comm_ring
1190
free_ring_pempty_equiv_int
1191
free_ring_punit_equiv_polynomial_int
1192
free_semigroup
1193
free_semigroup.lift
1194
free_semigroup.lift'
1195
free_semigroup.map
1196
free_semigroup.of
1197
free_semigroup.traverse
1198
free_semigroup.traverse'
1199
free_semigroup_free_magma
1200
function.bicompl
1201
function.bicompr
1202
function.embedding
1203
function.embedding.Pi_congr_right
1204
function.embedding.arrow_congr_left
1205
function.embedding.arrow_congr_right
1206
function.embedding.congr
1207
function.embedding.equiv_of_surjective
1208
function.embedding.image
1209
function.embedding.of_not_nonempty
1210
function.embedding.of_surjective
1211
function.embedding.prod_congr
1212
function.embedding.refl
1213
function.embedding.set_value
1214
function.embedding.sigma_congr_right
1215
function.embedding.subtype
1216
function.embedding.subtype_map
1217
function.embedding.sum_congr
1218
function.embedding.trans
1219
function.injective.decidable_eq
1220
function.involutive.to_equiv
1221
function.restrict
1222
function.uncurry'
1223
functor.add_const
1224
functor.add_const.mk
1225
functor.add_const.run
1226
functor.comp.map
1227
functor.comp.mk
1228
functor.comp.run
1229
functor.const.mk
1230
functor.const.mk'
1231
functor.const.run
1232
functor.map_equiv
1233
gaussian_int
1234
gaussian_int.div
1235
gaussian_int.mod
1236
gaussian_int.to_complex
1237
ge.is_antisymm
1238
ge.is_linear_order
1239
ge.is_partial_order
1240
ge.is_preorder
1241
ge.is_refl
1242
ge.is_total
1243
ge.is_total_preorder
1244
ge.is_trans
1245
ge_from_le
1246
ge_iff_le
1247
ge_of_eq
1248
get_ext_subject
1249
gmultiples
1250
gpowers
1251
group.in_closure
1252
gsmul
1253
gt.is_antisymm
1254
gt.is_asymm
1255
gt.is_irrefl
1256
gt.is_strict_order
1257
gt.is_trans
1258
gt.is_trichotomous
1259
gt_from_lt
1260
gt_iff_lt
1261
gt_of_mul_lt_mul_neg_right
1262
has_edist
1263
has_inner
1264
hash_map.mk_as_list
1265
hash_map.valid.modify
1266
hidden
1267
holor.assoc_left
1268
holor.assoc_right
1269
holor_index.assoc_left
1270
holor_index.assoc_right
1271
holor_index.drop
1272
holor_index.take
1273
homemorph.to_measurable_equiv
1274
homeomorph.add_left
1275
homeomorph.add_right
1276
homeomorph.homeomorph_of_continuous_open
1277
homeomorph.inv
1278
homeomorph.mul_left
1279
homeomorph.mul_right
1280
homeomorph.neg
1281
homeomorph.prod_assoc
1282
homeomorph.prod_comm
1283
homeomorph.prod_congr
1284
homeomorph.refl
1285
homeomorph.sigma_prod_distrib
1286
homeomorph.symm
1287
homeomorph.trans
1288
hyperreal.epsilon_lt_pos
1289
hyperreal.gt_of_neg_of_infinitesimal
1290
hyperreal.infinite_neg_mul_of_not_infinitesimal_pos_infinite_neg
1291
hyperreal.infinite_pos_def
1292
hyperreal.infinite_pos_iff_infinite_and_pos
1293
hyperreal.infinite_pos_iff_infinite_of_nonneg
1294
hyperreal.infinite_pos_iff_infinite_of_pos
1295
hyperreal.infinite_pos_iff_infinitesimal_inv_pos
1296
hyperreal.infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos
1297
hyperreal.infinitesimal_def
1298
hyperreal.infinitesimal_pos_iff_infinite_pos_inv
1299
hyperreal.is_st_iff_abs_sub_lt_delta
1300
hyperreal.lt_neg_of_pos_of_infinitesimal
1301
hyperreal.lt_of_pos_of_infinitesimal
1302
hyperreal.lt_of_tendsto_zero_of_pos
1303
hyperreal.neg_lt_of_tendsto_zero_of_pos
1304
hyperreal.pos_of_infinite_pos
1305
id.mk
1306
ideal
1307
ideal.closure
1308
ideal.is_coprime
1309
ideal.is_maximal
1310
ideal.is_prime
1311
ideal.is_principal
1312
ideal.is_principal.generator
1313
ideal.le_order_embedding_of_surjective
1314
ideal.lt_order_embedding_of_surjective
1315
ideal.map
1316
ideal.quotient
1317
ideal.quotient.lift
1318
ideal.quotient.map_mk
1319
ideal.quotient.mk
1320
ideal.quotient.nonzero_comm_ring
1321
ideal.quotient_inf_to_pi_quotient
1322
ideal.radical_pow
1323
ideal.span
1324
inducing
1325
infi_eq_elim
1326
infi_real_pos_eq_infi_nnreal_pos
1327
infinite
1328
infinite.nat_embedding
1329
initial_seg.le_add
1330
initial_seg.le_lt
1331
initial_seg.lt_or_eq
1332
int.bit_cases_on
1333
int.div_eq_div_of_mul_eq_mul
1334
int.eq_mul_div_of_mul_eq_mul_of_dvd_left
1335
int.even
1336
int.induction_on'
1337
int.modeq
1338
int.of_snum
1339
int.range
1340
int.shift2
1341
int.to_nat'
1342
integral_closure
1343
irrational
1344
is_absolute_value.mem_uniformity
1345
is_add_group_hom.ker
1346
is_add_group_hom.to_linear_map
1347
is_add_subgroup.add_center
1348
is_add_subgroup.add_normalizer
1349
is_add_subgroup.group_equiv_quotient_times_subgroup
1350
is_add_subgroup.left_coset_equiv_subgroup
1351
is_add_subgroup.mem_trivial
1352
is_add_subgroup.normalizer_is_add_subgroup
1353
is_add_subgroup.trivial
1354
is_basis.coord_fun
1355
is_basis.repr
1356
is_basis.to_dual_flip
1357
is_cau_of_decreasing_bounded
1358
is_cau_of_mono_bounded
1359
is_cau_seq.cauchy₂
1360
is_cau_seq.cauchy₃
1361
is_cau_series_of_abv_le_cau
1362
is_closed_map
1363
is_comm_applicative
1364
is_conj
1365
is_cyclic
1366
is_cyclic.comm_group
1367
is_group_hom.ker
1368
is_integral
1369
is_lawful_bifunctor
1370
is_lawful_bitraversable
1371
is_lawful_monad_cont
1372
is_lawful_traversable
1373
is_linear_map
1374
is_linear_map.mk'
1375
is_local_ring
1376
is_local_ring_hom
1377
is_noetherian
1378
is_noetherian_iff_well_founded
1379
is_noetherian_ring
1380
is_null_measurable
1381
is_ring_anti_hom
1382
is_ring_hom.ker
1383
is_ring_hom.to_module
1384
is_seq_closed
1385
is_subfield
1386
is_subgroup.center
1387
is_subgroup.group_equiv_quotient_times_subgroup
1388
is_subgroup.left_coset_equiv_subgroup
1389
is_subgroup.mem_trivial
1390
is_subgroup.normalizer
1391
is_subgroup.normalizer_is_subgroup
1392
lattice.Inf_eq_bot
1393
lattice.complete_lattice.copy
1394
lattice.conditionally_complete_linear_order
1395
lattice.conditionally_complete_linear_order_bot
1396
lattice.fixed_points
1397
lattice.fixed_points.next
1398
lattice.fixed_points.next_fixed
1399
lattice.fixed_points.prev
1400
lattice.fixed_points.prev_fixed
1401
lattice.infi_eq_bot
1402
lazy_list.list_equiv_lazy_list
1403
lazy_list.traverse
1404
le_of_forall_ge_of_dense
1405
le_of_forall_le_of_dense
1406
lean.parser.get_includes
1407
lean.parser.get_namespace
1408
lean.parser.get_variables
1409
lebesgue_number_lemma_of_metric
1410
lebesgue_number_lemma_of_metric_sUnion
1411
left_add_coset
1412
left_add_coset_equiv
1413
left_coset
1414
left_coset_equiv
1415
lex
1416
linarith.add_exprs
1417
linarith.add_exprs_aux
1418
linarith.add_neg_eq_pfs
1419
linarith.cast_expr
1420
linarith.comp.add
1421
linarith.comp.coeff_of
1422
linarith.comp.is_contr
1423
linarith.comp.lt
1424
linarith.comp.scale
1425
linarith.comp_source
1426
linarith.comp_source.flatten
1427
linarith.comp_source.to_string
1428
linarith.elab_arg_list
1429
linarith.elim_all_vars
1430
linarith.elim_with_set
1431
linarith.expr_contains
1432
linarith.find_cancel_factor
1433
linarith.find_contr
1434
linarith.get_comps
1435
linarith.get_contr_lemma_name
1436
linarith.get_nat_comps
1437
linarith.get_rel_sides
1438
linarith.get_var_list
1439
linarith.get_vars
1440
linarith.guard_is_nat_prop
1441
linarith.guard_is_strict_int_prop
1442
linarith.ineq
1443
linarith.ineq.is_lt
1444
linarith.ineq.max
1445
linarith.ineq.to_string
1446
linarith.ineq_const_mul_nm
1447
linarith.ineq_const_nm
1448
linarith.ineq_pf_tp
1449
linarith.is_nat_int_coe
1450
linarith.is_numeric
1451
linarith.linarith_config
1452
linarith.linarith_monad
1453
linarith.linarith_monad.run
1454
linarith.list.mfind
1455
linarith.map_lt
1456
linarith.map_of_expr_mul_aux
1457
linarith.mk_cast_eq_and_nonneg_prfs
1458
linarith.mk_coe_nat_nonneg_prf
1459
linarith.mk_coe_nat_nonneg_prfs
1460
linarith.mk_int_pfs_of_nat_pf
1461
linarith.mk_lt_zero_pf_aux
1462
linarith.mk_neg_one_lt_zero_pf
1463
linarith.mk_non_strict_int_pf_of_strict_int_pf
1464
linarith.mk_prod_prf
1465
linarith.mk_single_comp_zero_pf
1466
linarith.monad.elim_var
1467
linarith.mul_eq
1468
linarith.mul_expr
1469
linarith.mul_neg
1470
linarith.mul_nonpos
1471
linarith.norm_hyp
1472
linarith.norm_hyp_aux
1473
linarith.parse_into_comp_and_expr
1474
linarith.partition_by_type
1475
linarith.partition_by_type_aux
1476
linarith.pcomp
1477
linarith.pcomp.add
1478
linarith.pcomp.is_contr
1479
linarith.pcomp.scale
1480
linarith.pelim_var
1481
linarith.preferred_type_of_goal
1482
linarith.rb_map.find_defeq
1483
linarith.rearr_comp
1484
linarith.rem_neg
1485
linarith.replace_nat_pfs
1486
linarith.replace_strict_int_pfs
1487
linarith.term_of_ineq_prf
1488
linarith.to_comp
1489
linarith.to_comp_fold
1490
linarith.update
1491
linarith.validate
1492
linear_equiv.to_equiv
1493
linear_equiv.to_linear_map
1494
linear_equiv_matrix
1495
linear_independent_monoid_hom
1496
linear_map
1497
linear_map.comp
1498
linear_map.compl₂
1499
linear_map.compr₂
1500
linear_map.flip
1501
linear_map.id
1502
linear_map.lcomp
1503
linear_map.lflip
1504
linear_map.llcomp
1505
linear_map.lsmul
1506
linear_map.map_finsupp_total
1507
linear_map.mk₂
1508
linear_map.to_bilin
1509
linear_order.lift
1510
list.choose
1511
list.choose_x
1512
list.comp_traverse
1513
list.erase_dupkeys
1514
list.erasep
1515
list.extractp
1516
list.find_indexes_aux
1517
list.forall₂
1518
list.func.add
1519
list.func.equiv
1520
list.func.get
1521
list.func.get_neg
1522
list.func.length_neg
1523
list.func.neg
1524
list.func.pointwise
1525
list.func.set
1526
list.func.sub
1527
list.head'
1528
list.insert_nth
1529
list.insert_nth_remove_nth_of_ge
1530
list.kextract
1531
list.kreplace
1532
list.lex
1533
list.map_head
1534
list.map_last
1535
list.map_with_index
1536
list.map_with_index_core
1537
list.mem_ext
1538
list.mmap_accuml
1539
list.mmap_accumr
1540
list.mpartition
1541
list.nodupkeys
1542
list.of_fn
1543
list.of_fn_aux
1544
list.of_fn_nth_val
1545
list.pairwise_gt_iota
1546
list.partition_map
1547
list.permutations_aux
1548
list.permutations_aux.rec
1549
list.permutations_aux2
1550
list.reduce_option
1551
list.reverse_rec_on
1552
list.revzip
1553
list.scanr_aux
1554
list.split_on_p_aux
1555
list.sublists'_aux
1556
list.sublists_aux
1557
list.sublists_aux₁
1558
list.sublists_len
1559
list.sublists_len_aux
1560
list.take'
1561
list.tfae
1562
list.to_alist
1563
list.to_finmap
1564
list.transpose_aux
1565
list.traverse
1566
lists
1567
lists.atom
1568
lists.induction_mut
1569
lists.is_list
1570
lists.mem
1571
lists.of'
1572
lists.of_list
1573
lists.to_list
1574
lists'
1575
lists'.cons
1576
lists'.of_list
1577
lists'.to_list
1578
loc.to_string
1579
loc.to_string_aux
1580
local_of_is_local_ring
1581
local_of_nonunits_ideal
1582
local_of_unique_max_ideal
1583
local_of_unit_or_unit_one_sub
1584
local_ring
1585
local_ring.nonunits_ideal
1586
local_ring.residue_field
1587
local_ring.residue_field.map
1588
localization.at_prime
1589
localization.away
1590
localization.away.inv_self
1591
localization.away.lift
1592
localization.away_to_away_right
1593
localization.equiv_of_equiv
1594
localization.fraction_ring.eq_zero_of_ne_zero_of_mul_eq_zero
1595
localization.fraction_ring.equiv_of_equiv
1596
localization.fraction_ring.inv_aux
1597
localization.fraction_ring.map
1598
localization.le_order_embedding
1599
localization.lift
1600
localization.lift'
1601
localization.map
1602
localization.mk
1603
localization.non_zero_divisors
1604
localization.r
1605
localized_attr
1606
localized_cmd
1607
locally_finite.realizer
1608
magma.free_semigroup
1609
magma.free_semigroup.lift
1610
magma.free_semigroup.map
1611
magma.free_semigroup.of
1612
magma.free_semigroup.r
1613
manifold_core.local_homeomorph
1614
manifold_core.to_manifold
1615
matrix
1616
matrix.col
1617
matrix.diagonal
1618
matrix.minor
1619
matrix.mul
1620
matrix.mul_vec
1621
matrix.row
1622
matrix.sub_down
1623
matrix.sub_down_left
1624
matrix.sub_down_right
1625
matrix.sub_left
1626
matrix.sub_right
1627
matrix.sub_up
1628
matrix.sub_up_left
1629
matrix.sub_up_right
1630
matrix.transpose
1631
matrix.vec_mul
1632
matrix.vec_mul_vec
1633
max_le_add_of_nonneg
1634
measurable_equiv.cast
1635
measurable_equiv.prod_comm
1636
measurable_equiv.prod_congr
1637
measurable_equiv.prod_sum_distrib
1638
measurable_equiv.refl
1639
measurable_equiv.set.image
1640
measurable_equiv.set.prod
1641
measurable_equiv.set.range
1642
measurable_equiv.set.range_inl
1643
measurable_equiv.set.range_inr
1644
measurable_equiv.set.singleton
1645
measurable_equiv.set.univ
1646
measurable_equiv.sum_congr
1647
measurable_equiv.sum_prod_distrib
1648
measurable_equiv.sum_prod_sum
1649
measurable_equiv.symm
1650
measurable_equiv.trans
1651
measurable_space
1652
measurable_space.dynkin_system.generate
1653
measurable_space.dynkin_system.of_measurable_space
1654
measurable_space.dynkin_system.restrict_on
1655
measurable_space.dynkin_system.to_measurable_space
1656
measurable_space.gi_generate_from
1657
measurable_space.mk_of_closure
1658
measure_theory.ae_eq_fun.add
1659
measure_theory.ae_eq_fun.neg
1660
measure_theory.ae_eq_fun.smul
1661
measure_theory.lintegral_eq_nnreal
1662
measure_theory.measure
1663
measure_theory.measure.integral
1664
measure_theory.measure.is_complete
1665
measure_theory.measure.map
1666
measure_theory.measure.of_measurable
1667
measure_theory.measure.with_density
1668
measure_theory.measure'
1669
measure_theory.outer_measure
1670
measure_theory.outer_measure.Inf_gen
1671
measure_theory.outer_measure.map
1672
measure_theory.outer_measure.sum
1673
measure_theory.outer_measure.to_measure
1674
measure_theory.outer_measure.trim
1675
measure_theory.simple_func.eapprox
1676
measure_theory.simple_func.fin_vol_supp
1677
measure_theory.simple_func.ite
1678
measure_theory.volume
1679
mem_uniformity_edist
1680
metric.Hausdorff_dist_le_of_inf_dist
1681
metric.cauchy_iff
1682
metric.cauchy_seq_iff
1683
metric.cauchy_seq_iff'
1684
metric.completion.mem_uniformity_dist
1685
metric.completion.uniformity_dist
1686
metric.completion.uniformity_dist'
1687
metric.continuous_iff
1688
metric.continuous_iff'
1689
metric.diam_ball
1690
metric.diam_closed_ball
1691
metric.diam_le_of_forall_dist_le
1692
metric.exists_ball_subset_ball
1693
metric.exists_delta_of_continuous
1694
metric.glue_premetric
1695
metric.glue_space
1696
metric.is_open_iff
1697
metric.mem_ball_self
1698
metric.mem_closed_ball_self
1699
metric.mem_closure_iff'
1700
metric.mem_closure_range_iff
1701
metric.mem_nhds_iff
1702
metric.mem_of_closed'
1703
metric.mem_uniformity_dist
1704
metric.mem_uniformity_edist
1705
metric.nhds_eq
1706
metric.pos_of_mem_ball
1707
metric.second_countable_of_almost_dense_set
1708
metric.second_countable_of_countable_discretization
1709
metric.sum.dist
1710
metric.tendsto_at_top
1711
metric.tendsto_nhds
1712
metric.to_glue_l
1713
metric.to_glue_r
1714
metric.totally_bounded_iff
1715
metric.totally_bounded_of_finite_discretization
1716
metric.uniform_continuous_iff
1717
metric.uniform_embedding_iff
1718
metric.uniform_embedding_iff'
1719
metric.uniformity_dist
1720
metric.uniformity_dist'
1721
metric.uniformity_edist'
1722
metric_space.induced
1723
metric_space.replace_uniformity
1724
min_le_add_of_nonneg_left
1725
min_le_add_of_nonneg_right
1726
module.End
1727
module.core
1728
module.direct_limit
1729
module.direct_limit.totalize
1730
module.of_core
1731
monad_cont
1732
monad_cont.goto
1733
monad_cont.label
1734
monoid.foldl.get
1735
monoid.foldl.mk
1736
monoid.foldl.of_free_monoid
1737
monoid.foldr
1738
monoid.foldr.get
1739
monoid.foldr.mk
1740
monoid.foldr.of_free_monoid
1741
monoid.mfoldl
1742
monoid.mfoldl.get
1743
monoid.mfoldl.mk
1744
monoid.mfoldl.of_free_monoid
1745
monoid.mfoldr
1746
monoid.mfoldr.get
1747
monoid.mfoldr.mk
1748
monoid.mfoldr.of_free_monoid
1749
monoid_hom.one
1750
monotonicity
1751
mtry
1752
mul_action.comp_hom
1753
mul_action.fixed_points
1754
mul_action.mul_left_cosets
1755
mul_action.orbit
1756
mul_action.orbit_equiv_quotient_stabilizer
1757
mul_action.orbit_rel
1758
mul_action.stabilizer
1759
mul_action.to_perm
1760
mul_equiv.to_equiv
1761
mul_mono_nonpos
1762
multiplicative
1763
multiplicity.finite
1764
multiplicity.finite_mul_aux
1765
multiset.choose
1766
multiset.choose_x
1767
multiset.decidable_exists_multiset
1768
multiset.decidable_forall_multiset
1769
multiset.le_inf
1770
multiset.length_ndinsert_of_mem
1771
multiset.length_ndinsert_of_not_mem
1772
multiset.pi.cons
1773
multiset.pi.empty
1774
multiset.powerset
1775
multiset.powerset_aux
1776
multiset.powerset_aux'
1777
multiset.powerset_len
1778
multiset.powerset_len_aux
1779
multiset.rec_on
1780
multiset.sections
1781
multiset.strong_induction_on
1782
multiset.subsingleton_equiv
1783
multiset.sum
1784
multiset.sup_le
1785
multiset.to_finsupp
1786
multiset.traverse
1787
mv_polynomial.R
1788
mv_polynomial.evalᵢ
1789
mv_polynomial.evalₗ
1790
mv_polynomial.indicator
1791
mv_polynomial.restrict_degree
1792
mv_polynomial.restrict_total_degree
1793
mv_power_series.inv
1794
mv_power_series.trunc_fun
1795
mzip_with
1796
mzip_with'
1797
name.last_string
1798
nat.cases
1799
nat.dist_eq_sub_of_ge
1800
nat.elim
1801
nat.even
1802
nat.galois_connection_mul_div
1803
nat.min_fac_aux
1804
nat.modeq.chinese_remainder
1805
nat.partrec
1806
nat.partrec.code
1807
nat.partrec.code.const
1808
nat.partrec.code.curry
1809
nat.partrec.code.encode_code
1810
nat.partrec.code.eval
1811
nat.partrec.code.evaln
1812
nat.partrec.code.id
1813
nat.partrec.code.of_nat_code
1814
nat.partrec'.vec
1815
nat.primrec'.vec
1816
nat.rfind
1817
nat.rfind_opt
1818
nat.rfind_x
1819
nat.sqrt_aux
1820
nat.subtype.denumerable
1821
nat.subtype.of_nat
1822
nat.subtype.succ
1823
nat.to_pexpr
1824
nat.totient
1825
nat.unpaired
1826
nat.xgcd_aux
1827
nnreal.le_of_forall_epsilon_le
1828
nnreal.le_of_real_iff_coe_le
1829
nnreal.of_real
1830
nnreal.of_real_lt_iff_lt_coe
1831
nonempty_interior_of_Union_of_closed
1832
nonneg_comm_group.to_decidable_linear_ordered_comm_group
1833
nonneg_ring.to_linear_nonneg_ring
1834
nonunits
1835
norm_cast.derive
1836
norm_num.derive
1837
norm_num.derive1
1838
norm_num.eval_div_ext
1839
norm_num.eval_ineq
1840
norm_num.eval_pow
1841
norm_num.eval_prime
1842
norm_num.min_fac_helper
1843
norm_num.prove_lt
1844
norm_num.prove_min_fac
1845
norm_num.prove_non_prime
1846
norm_num.prove_pos
1847
normal_add_subgroup
1848
normal_of_eq_add_cosets
1849
normal_of_eq_cosets
1850
normal_subgroup
1851
normalize
1852
normed_group.tendsto_nhds_zero
1853
not.elim
1854
null_measurable
1855
num.add
1856
num.bit
1857
num.bit0
1858
num.bit1
1859
num.cmp
1860
num.cmp_to_nat
1861
num.div
1862
num.div2
1863
num.gcd
1864
num.gcd_aux
1865
num.land
1866
num.ldiff
1867
num.lor
1868
num.lxor
1869
num.mod
1870
num.mul
1871
num.nat_size
1872
num.of_nat'
1873
num.of_znum
1874
num.of_znum'
1875
num.one_bits
1876
num.ppred
1877
num.pred
1878
num.psub
1879
num.shiftl
1880
num.shiftr
1881
num.size
1882
num.sub
1883
num.sub'
1884
num.succ
1885
num.succ'
1886
num.test_bit
1887
num.to_znum
1888
num.to_znum_neg
1889
num.transfer
1890
num.transfer_rw
1891
nzsnum.bit0
1892
nzsnum.bit1
1893
nzsnum.drec'
1894
nzsnum.head
1895
nzsnum.not
1896
nzsnum.sign
1897
nzsnum.tail
1898
obviously.attr
1899
old_conv
1900
old_conv.apply
1901
old_conv.apply'
1902
old_conv.apply_lemmas
1903
old_conv.apply_lemmas_core
1904
old_conv.apply_propext_lemmas
1905
old_conv.apply_propext_lemmas_core
1906
old_conv.apply_propext_simp_set
1907
old_conv.apply_simp_set
1908
old_conv.applyc
1909
old_conv.bind
1910
old_conv.bottom_up
1911
old_conv.change
1912
old_conv.congr
1913
old_conv.congr_arg
1914
old_conv.congr_binder
1915
old_conv.congr_core
1916
old_conv.congr_fun
1917
old_conv.congr_rule
1918
old_conv.conversion
1919
old_conv.current_relation
1920
old_conv.dsimp
1921
old_conv.execute
1922
old_conv.fail
1923
old_conv.failed
1924
old_conv.find
1925
old_conv.find_pattern
1926
old_conv.findp
1927
old_conv.first
1928
old_conv.funext
1929
old_conv.funext'
1930
old_conv.head_beta
1931
old_conv.interactive.change
1932
old_conv.interactive.dsimp
1933
old_conv.interactive.find
1934
old_conv.interactive.itactic
1935
old_conv.interactive.trace_state
1936
old_conv.interactive.whnf
1937
old_conv.istep
1938
old_conv.lhs
1939
old_conv.lift_tactic
1940
old_conv.map
1941
old_conv.match_expr
1942
old_conv.match_pattern
1943
old_conv.mk_match_expr
1944
old_conv.orelse
1945
old_conv.propext'
1946
old_conv.pure
1947
old_conv.repeat
1948
old_conv.save_info
1949
old_conv.seq
1950
old_conv.skip
1951
old_conv.step
1952
old_conv.to_tactic
1953
old_conv.top_down
1954
old_conv.trace
1955
old_conv.trace_lhs
1956
old_conv.whnf
1957
old_conv_result
1958
omega.abort
1959
omega.add_ee
1960
omega.cancel
1961
omega.clause
1962
omega.clause.append
1963
omega.clause.holds
1964
omega.clause.sat
1965
omega.clause.unsat
1966
omega.clauses.sat
1967
omega.clauses.unsat
1968
omega.clear_unused_hyp
1969
omega.clear_unused_hyps
1970
omega.coeffs.val
1971
omega.coeffs.val_between
1972
omega.coeffs.val_except
1973
omega.coeffs_reduce
1974
omega.ee
1975
omega.ee.repr
1976
omega.ee_commit
1977
omega.ee_state
1978
omega.elim_eq
1979
omega.elim_eqs
1980
omega.elim_var
1981
omega.elim_var_aux
1982
omega.eq_elim
1983
omega.eqelim
1984
omega.factor
1985
omega.find_ees
1986
omega.find_min_coeff
1987
omega.find_min_coeff_core
1988
omega.find_neg_const
1989
omega.find_scalars
1990
omega.find_scalars_core
1991
omega.form_domain
1992
omega.form_wf
1993
omega.gcd
1994
omega.get_ees
1995
omega.get_eqs
1996
omega.get_gcd
1997
omega.get_les
1998
omega.goal_domain
1999
omega.goal_domain_aux
2000
omega.head_eq
2001
omega.int.canonize
2002
omega.int.desugar
2003
omega.int.dnf
2004
omega.int.dnf_core
2005
omega.int.form
2006
omega.int.form.equiv
2007
omega.int.form.fresh_index
2008
omega.int.form.holds
2009
omega.int.form.implies
2010
omega.int.form.induce
2011
omega.int.form.repr
2012
omega.int.form.sat
2013
omega.int.form.unsat
2014
omega.int.form.valid
2015
omega.int.is_nnf
2016
omega.int.neg_elim
2017
omega.int.neg_free
2018
omega.int.nnf
2019
omega.int.preterm
2020
omega.int.preterm.add_one
2021
omega.int.preterm.fresh_index
2022
omega.int.preterm.repr
2023
omega.int.preterm.val
2024
omega.int.prove_lia
2025
omega.int.prove_univ_close
2026
omega.int.push_neg
2027
omega.int.to_form
2028
omega.int.to_form_core
2029
omega.int.to_preterm
2030
omega.int.univ_close
2031
omega.is_lia_form
2032
omega.is_lia_term
2033
omega.is_lna_form
2034
omega.is_lna_term
2035
omega.lin_comb
2036
omega.nat.bools.or
2037
omega.nat.canonize
2038
omega.nat.desugar
2039
omega.nat.dnf
2040
omega.nat.dnf_core
2041
omega.nat.form
2042
omega.nat.form.equiv
2043
omega.nat.form.fresh_index
2044
omega.nat.form.holds
2045
omega.nat.form.implies
2046
omega.nat.form.induce
2047
omega.nat.form.neg_free
2048
omega.nat.form.repr
2049
omega.nat.form.sat
2050
omega.nat.form.sub_free
2051
omega.nat.form.sub_subst
2052
omega.nat.form.sub_terms
2053
omega.nat.form.unsat
2054
omega.nat.form.valid
2055
omega.nat.is_diff
2056
omega.nat.is_nnf
2057
omega.nat.neg_elim
2058
omega.nat.neg_elim_core
2059
omega.nat.nnf
2060
omega.nat.nonneg_consts
2061
omega.nat.nonneg_consts_core
2062
omega.nat.nonnegate
2063
omega.nat.preterm
2064
omega.nat.preterm.add_one
2065
omega.nat.preterm.fresh_index
2066
omega.nat.preterm.induce
2067
omega.nat.preterm.prove_sub_free
2068
omega.nat.preterm.repr
2069
omega.nat.preterm.sub_free
2070
omega.nat.preterm.sub_subst
2071
omega.nat.preterm.sub_terms
2072
omega.nat.preterm.val
2073
omega.nat.prove_lna
2074
omega.nat.prove_neg_free
2075
omega.nat.prove_sub_free
2076
omega.nat.prove_univ_close
2077
omega.nat.prove_unsat_neg_free
2078
omega.nat.prove_unsat_sub_free
2079
omega.nat.push_neg
2080
omega.nat.sub_elim
2081
omega.nat.sub_elim_core
2082
omega.nat.sub_fresh_index
2083
omega.nat.term.vars
2084
omega.nat.term.vars_core
2085
omega.nat.terms.vars
2086
omega.nat.to_form
2087
omega.nat.to_form_core
2088
omega.nat.to_preterm
2089
omega.nat.univ_close
2090
omega.preprocess
2091
omega.prove_forall_mem_eq_zero
2092
omega.prove_neg
2093
omega.prove_unsat
2094
omega.prove_unsat_ef
2095
omega.prove_unsat_lin_comb
2096
omega.prove_unsats
2097
omega.rev_lia
2098
omega.rev_lna
2099
omega.revert_cond
2100
omega.revert_cond_all
2101
omega.rhs
2102
omega.run
2103
omega.select_domain
2104
omega.set_ees
2105
omega.set_eqs
2106
omega.set_les
2107
omega.sgm
2108
omega.subst
2109
omega.sym_sym
2110
omega.symdiv
2111
omega.symmod
2112
omega.term
2113
omega.term.add
2114
omega.term.div
2115
omega.term.fresh_index
2116
omega.term.mul
2117
omega.term.neg
2118
omega.term.sub
2119
omega.term.to_string
2120
omega.term.val
2121
omega.term_domain
2122
omega.terms.fresh_index
2123
omega.trisect
2124
omega.type_domain
2125
omega.unsat_lin_comb
2126
omega.update
2127
omega.update_zero
2128
omega_int
2129
omega_nat
2130
onote.oadd_lt_oadd_1
2131
onote.oadd_lt_oadd_2
2132
onote.oadd_lt_oadd_3
2133
onote.power_aux
2134
onote.to_string_aux1
2135
open_add_subgroup
2136
open_add_subgroup.sum
2137
open_locale_cmd
2138
open_subgroup.prod
2139
opposite.op
2140
opposite.op_induction
2141
opposite.unop
2142
opt_minus
2143
option.cases_on'
2144
option.comp_traverse
2145
option.lift_or_get
2146
option.rel
2147
option.to_list
2148
option.traverse
2149
option_t.call_cc
2150
option_t.mk_label
2151
option_t.pass_aux
2152
order_embedding.collapse_F
2153
order_embedding.lt_embedding_of_le_embedding
2154
order_embedding.nat_gt
2155
order_embedding.nat_lt
2156
order_embedding.refl
2157
order_embedding.trans
2158
order_embedding.well_founded_iff_no_descending_seq
2159
order_iso.of_surjective
2160
order_iso.prod_lex_congr
2161
order_iso.refl
2162
order_iso.sum_lex_congr
2163
order_iso.symm
2164
order_iso.to_order_embedding
2165
order_iso.trans
2166
order_of_pos
2167
ordering.compares.eq_gt
2168
ordinal.CNF_rec
2169
ordinal.CNF_sorted
2170
ordinal.add_absorp_iff
2171
ordinal.initial_seg_out
2172
ordinal.lift.initial_seg
2173
ordinal.lift.principal_seg
2174
ordinal.limit_rec_on
2175
ordinal.order_iso_out
2176
ordinal.principal_seg_out
2177
ordinal.typein.principal_seg
2178
ordinal.typein_iso
2179
ordinal.unbounded_range_of_sup_ge
2180
pSet.definable.eq_mk
2181
pSet.definable.resp
2182
pSet.resp.equiv
2183
pSet.resp.eval_aux
2184
pSet.resp.f
2185
pSet.subset
2186
padic.complete'
2187
padic.exi_rat_seq_conv
2188
padic.lim_seq
2189
padic.padic_norm_e_lim_le
2190
padic.rat_dense
2191
padic.rat_dense'
2192
padic_norm.neg
2193
padic_norm_e.defn
2194
padic_norm_e.nonneg
2195
padic_norm_e.rat_norm
2196
padic_norm_z
2197
padic_seq
2198
padic_seq.norm_nonneg
2199
padic_seq.stationary_point_spec
2200
partial_order.lift
2201
partrec
2202
partrec₂
2203
pell.asq_pos
2204
pell.az
2205
pell.d_pos
2206
pell.dnsq
2207
pell.dvd_of_ysq_dvd
2208
pell.dz_val
2209
pell.eq_of_xn_modeq
2210
pell.eq_of_xn_modeq'
2211
pell.eq_of_xn_modeq_le
2212
pell.eq_of_xn_modeq_lem1
2213
pell.eq_of_xn_modeq_lem2
2214
pell.eq_of_xn_modeq_lem3
2215
pell.eq_pell
2216
pell.eq_pell_lem
2217
pell.eq_pell_zd
2218
pell.eq_pow_of_pell
2219
pell.eq_pow_of_pell_lem
2220
pell.is_pell
2221
pell.is_pell_conj
2222
pell.is_pell_mul
2223
pell.is_pell_nat
2224
pell.is_pell_norm
2225
pell.is_pell_one
2226
pell.is_pell_pell_zd
2227
pell.matiyasevic
2228
pell.modeq_of_xn_modeq
2229
pell.n_lt_a_pow
2230
pell.n_lt_xn
2231
pell.pell_eq
2232
pell.pell_eqz
2233
pell.pell_val
2234
pell.pell_zd
2235
pell.pell_zd_add
2236
pell.pell_zd_im
2237
pell.pell_zd_re
2238
pell.pell_zd_sub
2239
pell.pell_zd_succ
2240
pell.pell_zd_succ_succ
2241
pell.x_increasing
2242
pell.x_pos
2243
pell.x_sub_y_dvd_pow
2244
pell.x_sub_y_dvd_pow_lem
2245
pell.xn
2246
pell.xn_add
2247
pell.xn_ge_a_pow
2248
pell.xn_modeq_x2n_add
2249
pell.xn_modeq_x2n_add_lem
2250
pell.xn_modeq_x2n_sub
2251
pell.xn_modeq_x2n_sub_lem
2252
pell.xn_modeq_x4n_add
2253
pell.xn_modeq_x4n_sub
2254
pell.xn_one
2255
pell.xn_succ
2256
pell.xn_succ_succ
2257
pell.xn_zero
2258
pell.xy_coprime
2259
pell.xy_modeq_of_modeq
2260
pell.xy_modeq_yn
2261
pell.xy_succ_succ
2262
pell.xz
2263
pell.xz_sub
2264
pell.xz_succ
2265
pell.xz_succ_succ
2266
pell.y_dvd_iff
2267
pell.y_increasing
2268
pell.y_mul_dvd
2269
pell.yn
2270
pell.yn_add
2271
pell.yn_ge_n
2272
pell.yn_modeq_a_sub_one
2273
pell.yn_modeq_two
2274
pell.yn_one
2275
pell.yn_succ
2276
pell.yn_succ_succ
2277
pell.yn_zero
2278
pell.ysq_dvd_yy
2279
pell.yz
2280
pell.yz_sub
2281
pell.yz_succ
2282
pell.yz_succ_succ
2283
pempty.elim
2284
pequiv.matrix_mul_apply
2285
pequiv.mul_matrix_apply
2286
pequiv.of_set
2287
pequiv.refl
2288
pequiv.single
2289
pequiv.single_mul_single_right
2290
pequiv.symm
2291
pequiv.to_matrix
2292
pequiv.trans
2293
pequiv.trans_single_of_eq_none
2294
perfect_closure.UMP
2295
perfect_closure.eq_iff'
2296
perfect_closure.frobenius_equiv
2297
perfect_closure.has_inv
2298
perfect_closure.of
2299
perfect_closure.r
2300
perms_of_finset
2301
perms_of_list
2302
pexpr.get_uninst_pis
2303
pfun.core
2304
pfun.equiv_subtype
2305
pfun.fix
2306
pfun.fix_induction
2307
pfun.graph'
2308
pfun.image
2309
pfun.preimage
2310
pfun.res
2311
pgame.add_lt_add
2312
pgame.numeric.lt_move_right
2313
pgame.numeric.move_left_lt
2314
pi.lex
2315
pi.linear_independent_std_basis
2316
pilex
2317
pmf.bernoulli
2318
pmf.bind
2319
pmf.map
2320
pmf.of_fintype
2321
pmf.of_multiset
2322
pmf.pure
2323
pmf.seq
2324
pmf.support
2325
pnat.div
2326
pnat.div_exact
2327
pnat.gcd
2328
pnat.gcd_a'
2329
pnat.gcd_b'
2330
pnat.gcd_d
2331
pnat.gcd_w
2332
pnat.gcd_x
2333
pnat.gcd_y
2334
pnat.gcd_z
2335
pnat.lcm
2336
pnat.mod
2337
pnat.mod_div
2338
pnat.prime
2339
pnat.xgcd
2340
pnat.xgcd_type.a
2341
pnat.xgcd_type.b
2342
pnat.xgcd_type.finish
2343
pnat.xgcd_type.flip
2344
pnat.xgcd_type.is_reduced'
2345
pnat.xgcd_type.is_special'
2346
pnat.xgcd_type.mk'
2347
pnat.xgcd_type.q
2348
pnat.xgcd_type.qp
2349
pnat.xgcd_type.r
2350
pnat.xgcd_type.succ₂
2351
pnat.xgcd_type.v
2352
pnat.xgcd_type.w
2353
pnat.xgcd_type.z
2354
polynomial.binom_expansion
2355
polynomial.coeff_coe_to_fun
2356
polynomial.comp
2357
polynomial.decidable_dvd_monic
2358
polynomial.degree_eq_iff_nat_degree_eq_of_pos
2359
polynomial.div
2360
polynomial.div_mod_by_monic_aux
2361
polynomial.eval_sub_factor
2362
polynomial.eval₂_zero
2363
polynomial.lcoeff
2364
polynomial.map_injective
2365
polynomial.mod
2366
polynomial.monomial
2367
polynomial.nonzero_comm_ring.of_polynomial_ne
2368
polynomial.nonzero_comm_semiring.of_polynomial_ne
2369
polynomial.pow_add_expansion
2370
polynomial.pow_sub_pow_factor
2371
polynomial.rec_on_horner
2372
polynomial.root_multiplicity
2373
polynomial.splits
2374
polynomial.tendsto_infinity
2375
pos_num.add
2376
pos_num.bit
2377
pos_num.cmp
2378
pos_num.cmp_to_nat
2379
pos_num.div'
2380
pos_num.divmod
2381
pos_num.divmod_aux
2382
pos_num.is_one
2383
pos_num.land
2384
pos_num.ldiff
2385
pos_num.lor
2386
pos_num.lxor
2387
pos_num.mod'
2388
pos_num.mul
2389
pos_num.nat_size
2390
pos_num.of_nat
2391
pos_num.of_nat_succ
2392
pos_num.of_znum
2393
pos_num.of_znum'
2394
pos_num.one_bits
2395
pos_num.pred
2396
pos_num.pred'
2397
pos_num.pred_to_nat
2398
pos_num.shiftl
2399
pos_num.shiftr
2400
pos_num.size
2401
pos_num.sqrt_aux
2402
pos_num.sqrt_aux1
2403
pos_num.sub
2404
pos_num.sub'
2405
pos_num.succ
2406
pos_num.test_bit
2407
pos_num.transfer
2408
pos_num.transfer_rw
2409
power_series.inv
2410
power_series.inv.aux
2411
power_series.mk
2412
power_series.order_add_ge
2413
power_series.order_ge
2414
power_series.order_ge_nat
2415
power_series.order_mul_ge
2416
premetric_space
2417
preorder.lift
2418
primcodable.of_equiv
2419
primcodable.subtype
2420
prime_multiset.of_nat_multiset
2421
prime_multiset.of_pnat_list
2422
prime_multiset.of_pnat_multiset
2423
prime_multiset.prod
2424
prime_multiset.to_pnat_multiset
2425
principal_ideal_domain
2426
principal_ideal_domain.factors
2427
principal_seg
2428
principal_seg.equiv_lt
2429
principal_seg.lt_equiv
2430
principal_seg.lt_le
2431
principal_seg.top_lt_top
2432
principal_seg.trans
2433
principal_seg.trans_top
2434
prod.bitraverse
2435
prod.lex.decidable
2436
push_neg.normalize_negations
2437
push_neg.push_neg_at_goal
2438
push_neg.push_neg_at_hyp
2439
push_neg.whnf_reducible
2440
quot.hrec_on₂
2441
quotient.choice
2442
quotient.fin_choice
2443
quotient.fin_choice_aux
2444
quotient.hrec_on₂
2445
quotient.lift_on'
2446
quotient.lift_on₂'
2447
quotient.mk'
2448
quotient.out'
2449
quotient_add_group.eq_class_eq_left_coset
2450
quotient_add_group.inhabited
2451
quotient_add_group.ker_lift
2452
quotient_add_group.left_rel
2453
quotient_add_group.lift
2454
quotient_add_group.map
2455
quotient_add_group.mk
2456
quotient_add_group.quotient
2457
quotient_add_group.quotient_ker_equiv_of_surjective
2458
quotient_add_group.quotient_ker_equiv_range
2459
quotient_group.eq_class_eq_left_coset
2460
quotient_group.fintype
2461
quotient_group.inhabited
2462
quotient_group.left_rel
2463
quotient_group.lift
2464
quotient_group.map
2465
quotient_group.mk
2466
quotient_group.preimage_mk_equiv_subgroup_times_set
2467
quotient_group.quotient_ker_equiv_of_surjective
2468
quotient_group.quotient_ker_equiv_range
2469
rank
2470
rat.add
2471
rat.inv
2472
rat.le
2473
rat.mul
2474
rat.neg
2475
rat.nonneg
2476
rat.num_denom_cases_on
2477
rat.num_denom_cases_on'
2478
rat.repr
2479
rat.sqrt
2480
rat_add_continuous_lemma
2481
rat_inv_continuous_lemma
2482
rat_mul_continuous_lemma
2483
re_pred
2484
reader_t.call_cc
2485
reader_t.mk_label
2486
real
2487
real.Inf
2488
real.Sup
2489
real.comm_ring_aux
2490
real.cos
2491
real.cosh
2492
real.exp
2493
real.le
2494
real.le_mk_of_forall_le
2495
real.le_of_forall_epsilon_le
2496
real.mk
2497
real.mk_le_of_forall_le
2498
real.mk_near_of_forall_near
2499
real.of_near
2500
real.of_rat
2501
real.pi_gt_314
2502
real.pi_gt_sqrt_two_add_series
2503
real.pi_gt_three
2504
real.sin
2505
real.sinh
2506
real.sqrt
2507
real.sqrt_aux
2508
real.sqrt_two_add_series_nonneg
2509
real.sqrt_two_add_series_zero_nonneg
2510
real.tan
2511
real.tanh
2512
relation.comp
2513
relation.join
2514
relation.map
2515
relator.bi_total
2516
relator.bi_unique
2517
relator.left_total
2518
relator.left_unique
2519
relator.lift_fun
2520
relator.right_total
2521
relator.right_unique
2522
restate_axiom_cmd
2523
right_add_coset
2524
right_coset
2525
ring.closure
2526
ring.direct_limit
2527
ring_anti_equiv.refl
2528
ring_equiv
2529
ring_equiv.to_add_equiv
2530
ring_equiv.to_equiv
2531
ring_equiv.to_mul_equiv
2532
ring_hom.to_add_monoid_hom
2533
ring_hom.to_monoid_hom
2534
ring_invo.id
2535
ring_invo.to_ring_anti_equiv
2536
roption.equiv_option
2537
roption.get_or_else
2538
roption.restrict
2539
saturate_fun
2540
semiquot.bind
2541
semiquot.get
2542
semiquot.is_pure
2543
semiquot.map
2544
separated
2545
seq.bisim_o
2546
seq.cases_on
2547
seq.corec.F
2548
seq.is_bisimulation
2549
seq.mem
2550
sequence
2551
set.Union_eq_sigma_of_disjoint
2552
set.add_comm_monoid
2553
set.bUnion_eq_sigma_of_disjoint
2554
set.centralizer.add_submonoid
2555
set.comm_monoid
2556
set.countable.to_encodable
2557
set.enumerate
2558
set.fintype_bUnion
2559
set.fintype_bind
2560
set.fintype_insert'
2561
set.fintype_of_fintype_image
2562
set.fintype_subset
2563
set.kern_image
2564
set.pairwise_disjoint
2565
set.pi
2566
set.pointwise_add
2567
set.pointwise_add_add_monoid
2568
set.pointwise_add_add_semigroup
2569
set.pointwise_add_fintype
2570
set.pointwise_inv
2571
set.pointwise_mul
2572
set.pointwise_mul_action
2573
set.pointwise_mul_comm_semiring
2574
set.pointwise_mul_fintype
2575
set.pointwise_mul_monoid
2576
set.pointwise_mul_semigroup
2577
set.pointwise_mul_semiring
2578
set.pointwise_neg
2579
set.pointwise_one
2580
set.pointwise_zero
2581
set.seq
2582
set.sigma_to_Union
2583
set_fintype
2584
setoid.is_partition
2585
side
2586
side.other
2587
side.to_string
2588
simple_add_group
2589
simple_group
2590
snum.add
2591
snum.bit
2592
snum.bit0
2593
snum.bit1
2594
snum.bits
2595
snum.cadd
2596
snum.czadd
2597
snum.drec'
2598
snum.head
2599
snum.mul
2600
snum.neg
2601
snum.not
2602
snum.pred
2603
snum.rec'
2604
snum.sign
2605
snum.sub
2606
snum.succ
2607
snum.tail
2608
snum.test_bit
2609
state_t.call_cc
2610
state_t.mk_label
2611
strict_order.cof
2612
string.ltb
2613
string.map_tokens
2614
string.over_list
2615
string.split_on
2616
subalgebra
2617
subalgebra.comap
2618
subalgebra.fg
2619
subalgebra.to_submodule
2620
subalgebra.under
2621
subalgebra.val
2622
subgroup_units_cyclic
2623
submodule.annihilator
2624
submodule.colon
2625
submodule.fg
2626
submodule.subtype
2627
subrel.order_embedding
2628
subtype.restrict
2629
succeeds
2630
sum.bind
2631
sum.bitraverse
2632
sum.comp_traverse
2633
sum.elim
2634
sum.map
2635
sum.traverse
2636
sum.traverse_map
2637
sum_fin_sum_equiv
2638
summable_iff_vanishing_norm
2639
supr_eq_elim
2640
surreal.add
2641
swap_right
2642
sylow.fixed_points_mul_left_cosets_equiv_quotient
2643
sylow.mk_vector_prod_eq_one
2644
sylow.rotate_vectors_prod_eq_one
2645
sylow.vectors_prod_eq_one
2646
tactic.abel.add_g
2647
tactic.abel.cache
2648
tactic.abel.cache.app
2649
tactic.abel.cache.iapp
2650
tactic.abel.cache.int_to_expr
2651
tactic.abel.cache.mk_app
2652
tactic.abel.cache.mk_term
2653
tactic.abel.eval
2654
tactic.abel.eval'
2655
tactic.abel.eval_add
2656
tactic.abel.eval_atom
2657
tactic.abel.eval_neg
2658
tactic.abel.eval_smul
2659
tactic.abel.mk_cache
2660
tactic.abel.normal_expr
2661
tactic.abel.normal_expr.e
2662
tactic.abel.normal_expr.pp
2663
tactic.abel.normal_expr.refl_conv
2664
tactic.abel.normal_expr.term'
2665
tactic.abel.normal_expr.to_list
2666
tactic.abel.normal_expr.to_string
2667
tactic.abel.normal_expr.zero'
2668
tactic.abel.normalize
2669
tactic.abel.normalize_mode
2670
tactic.abel.smul
2671
tactic.abel.smulg
2672
tactic.abel.term
2673
tactic.abel.termg
2674
tactic.abstract_if_success
2675
tactic.add_coinductive_predicate
2676
tactic.add_coinductive_predicate.coind_pred
2677
tactic.add_coinductive_predicate.coind_pred.add_theorem
2678
tactic.add_coinductive_predicate.coind_pred.construct
2679
tactic.add_coinductive_predicate.coind_pred.corec_functional
2680
tactic.add_coinductive_predicate.coind_pred.destruct
2681
tactic.add_coinductive_predicate.coind_pred.func
2682
tactic.add_coinductive_predicate.coind_pred.func_g
2683
tactic.add_coinductive_predicate.coind_pred.f₁_l
2684
tactic.add_coinductive_predicate.coind_pred.f₂_l
2685
tactic.add_coinductive_predicate.coind_pred.impl_locals
2686
tactic.add_coinductive_predicate.coind_pred.impl_params
2687
tactic.add_coinductive_predicate.coind_pred.le
2688
tactic.add_coinductive_predicate.coind_pred.mono
2689
tactic.add_coinductive_predicate.coind_pred.pred
2690
tactic.add_coinductive_predicate.coind_pred.pred_g
2691
tactic.add_coinductive_predicate.coind_pred.rec'
2692
tactic.add_coinductive_predicate.coind_pred.u_params
2693
tactic.add_coinductive_predicate.coind_rule
2694
tactic.add_edge
2695
tactic.add_refl
2696
tactic.add_symm_proof
2697
tactic.alias.alias_attr
2698
tactic.alias.alias_cmd
2699
tactic.alias.alias_direct
2700
tactic.alias.alias_iff
2701
tactic.alias.get_alias_target
2702
tactic.alias.get_lambda_body
2703
tactic.alias.make_left_right
2704
tactic.alias.mk_iff_mp_app
2705
tactic.all_rewrites_using
2706
tactic.ancestor_attr
2707
tactic.apply_mod_cast
2708
tactic.assert_fresh
2709
tactic.assertv_fresh
2710
tactic.assoc_refl
2711
tactic.assoc_refl'
2712
tactic.assoc_rewrite
2713
tactic.assoc_rewrite_hyp
2714
tactic.assoc_rewrite_intl
2715
tactic.assoc_rewrite_target
2716
tactic.assoc_root
2717
tactic.assumption_mod_cast
2718
tactic.assumption_symm
2719
tactic.assumption_with
2720
tactic.calculated_Prop
2721
tactic.chain
2722
tactic.chain_core
2723
tactic.chain_eq_trans
2724
tactic.coinductive_predicate
2725
tactic.constr_to_prop
2726
tactic.contradiction_symm
2727
tactic.contradiction_with
2728
tactic.def_replacer_cmd
2729
tactic.derive_field
2730
tactic.derive_field_subtype
2731
tactic.derive_reassoc_proof
2732
tactic.elide.replace
2733
tactic.elide.unelide
2734
tactic.enum_assoc_subexpr
2735
tactic.enum_assoc_subexpr'
2736
tactic.exact_mod_cast
2737
tactic.explode
2738
tactic.explode.append_dep
2739
tactic.explode.args
2740
tactic.explode.core
2741
tactic.explode.entries
2742
tactic.explode.entries.add
2743
tactic.explode.entries.find
2744
tactic.explode.entries.head
2745
tactic.explode.entries.size
2746
tactic.explode.entry
2747
tactic.explode.format_aux
2748
tactic.explode.head'
2749
tactic.explode.may_be_proof
2750
tactic.explode.pad_right
2751
tactic.explode.status
2752
tactic.explode_cmd
2753
tactic.explode_expr
2754
tactic.expr_list_to_list_expr
2755
tactic.ext
2756
tactic.ext1
2757
tactic.ext_parse
2758
tactic.ext_patt
2759
tactic.fill_args
2760
tactic.fin_cases_at
2761
tactic.fin_cases_at_aux
2762
tactic.find_ancestors
2763
tactic.find_eq_type
2764
tactic.find_if_cond
2765
tactic.find_if_cond_at
2766
tactic.flatten
2767
tactic.generalize_proofs
2768
tactic.get_ancestors
2769
tactic.get_lift_prf
2770
tactic.get_nth_rewrite
2771
tactic.goals
2772
tactic.interactive.abel.mode
2773
tactic.interactive.ac_mono_ctx
2774
tactic.interactive.ac_mono_ctx.to_tactic_format
2775
tactic.interactive.ac_mono_ctx'
2776
tactic.interactive.ac_mono_ctx'.map
2777
tactic.interactive.ac_mono_ctx'.traverse
2778
tactic.interactive.ac_mono_ctx_ne
2779
tactic.interactive.ac_monotonicity_goal
2780
tactic.interactive.ac_refine
2781
tactic.interactive.apply_iff_congr_core
2782
tactic.interactive.apply_normed
2783
tactic.interactive.apply_rel
2784
tactic.interactive.arity
2785
tactic.interactive.as_goal
2786
tactic.interactive.assert_or_rule
2787
tactic.interactive.auto_simp_lemma
2788
tactic.interactive.best_match
2789
tactic.interactive.bin_op
2790
tactic.interactive.bin_op_left
2791
tactic.interactive.bin_op_right
2792
tactic.interactive.check_ac
2793
tactic.interactive.clean_ids
2794
tactic.interactive.coinduction
2795
tactic.interactive.collect_struct
2796
tactic.interactive.collect_struct'
2797
tactic.interactive.compact_decl
2798
tactic.interactive.compact_decl_aux
2799
tactic.interactive.compare
2800
tactic.interactive.congr_core'
2801
tactic.interactive.conv_lhs
2802
tactic.interactive.conv_rhs
2803
tactic.interactive.convert_to_core
2804
tactic.interactive.delete_expr
2805
tactic.interactive.derive_functor
2806
tactic.interactive.derive_lawful_functor
2807
tactic.interactive.derive_lawful_traversable
2808
tactic.interactive.derive_traverse
2809
tactic.interactive.field
2810
tactic.interactive.filter_instances
2811
tactic.interactive.find
2812
tactic.interactive.find_lemma
2813
tactic.interactive.find_one_difference
2814
tactic.interactive.find_rule
2815
tactic.interactive.fold_assoc
2816
tactic.interactive.fold_assoc1
2817
tactic.interactive.format_names
2818
tactic.interactive.fsplit
2819
tactic.interactive.functor_derive_handler
2820
tactic.interactive.functor_derive_handler'
2821
tactic.interactive.get_current_field
2822
tactic.interactive.get_equations_of
2823
tactic.interactive.get_monotonicity_lemmas
2824
tactic.interactive.get_operator
2825
tactic.interactive.guard_class
2826
tactic.interactive.guard_expr_eq'
2827
tactic.interactive.guard_hyp_nums
2828
tactic.interactive.guard_tags
2829
tactic.interactive.hide_meta_vars'
2830
tactic.interactive.higher_order_derive_handler
2831
tactic.interactive.injections_and_clear
2832
tactic.interactive.last_two
2833
tactic.interactive.lawful_functor_derive_handler
2834
tactic.interactive.lawful_functor_derive_handler'
2835
tactic.interactive.lawful_traversable_derive_handler
2836
tactic.interactive.lawful_traversable_derive_handler'
2837
tactic.interactive.list.minimum_on
2838
tactic.interactive.list_cast_of
2839
tactic.interactive.list_cast_of_aux
2840
tactic.interactive.loc.get_local_pp_names
2841
tactic.interactive.loc.get_local_uniq_names
2842
tactic.interactive.match_ac
2843
tactic.interactive.match_ac'
2844
tactic.interactive.match_chaining_rules
2845
tactic.interactive.match_imp
2846
tactic.interactive.match_prefix
2847
tactic.interactive.match_rule
2848
tactic.interactive.mk_congr_args
2849
tactic.interactive.mk_congr_law
2850
tactic.interactive.mk_fun_app
2851
tactic.interactive.mk_mapp'
2852
tactic.interactive.mk_mapp_aux'
2853
tactic.interactive.mk_one_instance
2854
tactic.interactive.mk_paragraph_aux
2855
tactic.interactive.mk_pattern
2856
tactic.interactive.mk_rel
2857
tactic.interactive.mono_aux
2858
tactic.interactive.mono_cfg
2859
tactic.interactive.mono_function
2860
tactic.interactive.mono_function.to_tactic_format
2861
tactic.interactive.mono_head_candidates
2862
tactic.interactive.mono_key
2863
tactic.interactive.mono_law
2864
tactic.interactive.mono_law.to_tactic_format
2865
tactic.interactive.mono_selection
2866
tactic.interactive.monotoncity.check
2867
tactic.interactive.monotoncity.check_rel
2868
tactic.interactive.monotonicity.attr
2869
tactic.interactive.obtain_parse
2870
tactic.interactive.old_conv
2871
tactic.interactive.one_line
2872
tactic.interactive.op_induction
2873
tactic.interactive.parse_ac_mono_function
2874
tactic.interactive.parse_ac_mono_function'
2875
tactic.interactive.parse_assoc_chain
2876
tactic.interactive.parse_assoc_chain'
2877
tactic.interactive.parse_config
2878
tactic.interactive.parse_list
2879
tactic.interactive.pi_head
2880
tactic.interactive.pi_instance
2881
tactic.interactive.rec.to_tactic_format
2882
tactic.interactive.record_lit
2883
tactic.interactive.refine_one
2884
tactic.interactive.refine_recursively
2885
tactic.interactive.rep_arity
2886
tactic.interactive.repeat_or_not
2887
tactic.interactive.repeat_until
2888
tactic.interactive.return_cast
2889
tactic.interactive.revert_all
2890
tactic.interactive.ring.mode
2891
tactic.interactive.same_function
2892
tactic.interactive.same_function_aux
2893
tactic.interactive.same_operator
2894
tactic.interactive.side
2895
tactic.interactive.side_conditions
2896
tactic.interactive.simp_functor
2897
tactic.interactive.solve_mvar
2898
tactic.interactive.source_fields
2899
tactic.interactive.squeeze_simp
2900
tactic.interactive.squeeze_simpa
2901
tactic.interactive.tfae_have
2902
tactic.interactive.traversable_derive_handler
2903
tactic.interactive.traversable_derive_handler'
2904
tactic.interactive.traversable_law_starter
2905
tactic.interactive.traverse_constructor
2906
tactic.interactive.traverse_field
2907
tactic.interactive.unify_with_instance
2908
tactic.interactive.with_prefix
2909
tactic.interactive.work_on_goal
2910
tactic.library_search_hole_cmd
2911
tactic.list_Pi
2912
tactic.list_Sigma
2913
tactic.local_cache.internal.block_local.clear
2914
tactic.local_cache.internal.block_local.get_name
2915
tactic.local_cache.internal.block_local.present
2916
tactic.local_cache.internal.block_local.try_get_name
2917
tactic.local_cache.internal.cache_scope
2918
tactic.local_cache.internal.def_local.FNV_OFFSET_BASIS
2919
tactic.local_cache.internal.def_local.FNV_PRIME
2920
tactic.local_cache.internal.def_local.RADIX
2921
tactic.local_cache.internal.def_local.apply_tag
2922
tactic.local_cache.internal.def_local.clear
2923
tactic.local_cache.internal.def_local.get_name
2924
tactic.local_cache.internal.def_local.get_root_name
2925
tactic.local_cache.internal.def_local.get_tag_with_status
2926
tactic.local_cache.internal.def_local.hash_byte
2927
tactic.local_cache.internal.def_local.hash_context
2928
tactic.local_cache.internal.def_local.hash_string
2929
tactic.local_cache.internal.def_local.is_name_dead
2930
tactic.local_cache.internal.def_local.kill_name
2931
tactic.local_cache.internal.def_local.mk_dead_name
2932
tactic.local_cache.internal.def_local.present
2933
tactic.local_cache.internal.def_local.try_get_name
2934
tactic.local_cache.internal.load_data
2935
tactic.local_cache.internal.mk_full_namespace
2936
tactic.local_cache.internal.poke_data
2937
tactic.local_cache.internal.run_once_under_name
2938
tactic.local_cache.internal.save_data
2939
tactic.match_assoc_pattern
2940
tactic.match_assoc_pattern'
2941
tactic.match_fn
2942
tactic.merge_list
2943
tactic.mk_assoc
2944
tactic.mk_assoc_instance
2945
tactic.mk_assoc_pattern
2946
tactic.mk_assoc_pattern'
2947
tactic.mk_congr_arg_using_dsimp'
2948
tactic.mk_eq_proof
2949
tactic.mk_iff
2950
tactic.mk_replacer
2951
tactic.mk_replacer₁
2952
tactic.mk_replacer₂
2953
tactic.mllist
2954
tactic.mllist.append
2955
tactic.mllist.bind_
2956
tactic.mllist.concat
2957
tactic.mllist.empty
2958
tactic.mllist.enum
2959
tactic.mllist.enum_from
2960
tactic.mllist.filter
2961
tactic.mllist.filter_map
2962
tactic.mllist.fix
2963
tactic.mllist.fixl
2964
tactic.mllist.fixl_with
2965
tactic.mllist.force
2966
tactic.mllist.head
2967
tactic.mllist.join
2968
tactic.mllist.m_of_list
2969
tactic.mllist.map
2970
tactic.mllist.mfilter
2971
tactic.mllist.mfilter_map
2972
tactic.mllist.mfirst
2973
tactic.mllist.mmap
2974
tactic.mllist.monad_lift
2975
tactic.mllist.of_list
2976
tactic.mllist.range
2977
tactic.mllist.squash
2978
tactic.mllist.take
2979
tactic.mllist.uncons
2980
tactic.modify_ref
2981
tactic.mono
2982
tactic.op_induction
2983
tactic.op_induction.find_opposite_hyp
2984
tactic.op_induction.is_opposite
2985
tactic.op_induction'
2986
tactic.perform_nth_rewrite
2987
tactic.prove_eqv_target
2988
tactic.rcases.continue
2989
tactic.rcases.process_constructors
2990
tactic.rcases_core
2991
tactic.rcases_hint
2992
tactic.rcases_hint.continue
2993
tactic.rcases_hint.process_constructors
2994
tactic.rcases_hint_core
2995
tactic.rcases_parse_depth
2996
tactic.rcases_patt
2997
tactic.rcases_patt.format
2998
tactic.rcases_patt.invert
2999
tactic.rcases_patt.invert'
3000
tactic.rcases_patt.invert_list
3001
tactic.rcases_patt.invert_many
3002
tactic.rcases_patt.merge
3003
tactic.rcases_patt.name
3004
tactic.rcases_patt_inverted.format
3005
tactic.rcases_patt_inverted.format_list
3006
tactic.rcases_patt_inverted.invert
3007
tactic.rcases_patt_inverted.invert_list
3008
tactic.rcases_patt_parse
3009
tactic.rcases_patt_parse_core
3010
tactic.rcases_patt_parse_list
3011
tactic.reduce_ifs_at
3012
tactic.refl_conv
3013
tactic.repeat_count
3014
tactic.repeat_with_results
3015
tactic.replaceable_attr
3016
tactic.replacer
3017
tactic.replacer_attr
3018
tactic.replacer_core
3019
tactic.rewrite_all.cfg
3020
tactic.rewrite_all.congr.app_map
3021
tactic.rewrite_all.congr.expr_lens
3022
tactic.rewrite_all.congr.expr_lens.congr
3023
tactic.rewrite_all.congr.expr_lens.replace
3024
tactic.rewrite_all.congr.expr_lens.to_sides
3025
tactic.rewrite_all.congr.expr_lens.to_tactic_string
3026
tactic.rewrite_all.congr.rewrite_all
3027
tactic.rewrite_all.congr.rewrite_all_lazy
3028
tactic.rewrite_all.congr.rewrite_at_lens
3029
tactic.rewrite_all.congr.rewrite_is_of_entire
3030
tactic.rewrite_all.congr.rewrite_without_new_mvars
3031
tactic.rewrite_all.tracked_rewrite
3032
tactic.rewrite_all.tracked_rewrite.eval
3033
tactic.rewrite_all.tracked_rewrite.replace_target
3034
tactic.rewrite_all.tracked_rewrite.replace_target_lhs
3035
tactic.rewrite_all.tracked_rewrite.replace_target_rhs
3036
tactic.ring.add_atom
3037
tactic.ring.cache
3038
tactic.ring.cache.cs_app
3039
tactic.ring.eval
3040
tactic.ring.eval'
3041
tactic.ring.eval_add
3042
tactic.ring.eval_atom
3043
tactic.ring.eval_const_mul
3044
tactic.ring.eval_horner
3045
tactic.ring.eval_mul
3046
tactic.ring.eval_neg
3047
tactic.ring.eval_pow
3048
tactic.ring.get_atom
3049
tactic.ring.get_cache
3050
tactic.ring.get_transparency
3051
tactic.ring.horner
3052
tactic.ring.horner_expr
3053
tactic.ring.horner_expr.e
3054
tactic.ring.horner_expr.pp
3055
tactic.ring.horner_expr.refl_conv
3056
tactic.ring.horner_expr.to_string
3057
tactic.ring.horner_expr.xadd'
3058
tactic.ring.lift
3059
tactic.ring.normalize
3060
tactic.ring.normalize_mode
3061
tactic.ring.ring_m
3062
tactic.ring.ring_m.mk_app
3063
tactic.ring.ring_m.run
3064
tactic.ring2.horner_expr.add
3065
tactic.ring2.horner_expr.add_aux
3066
tactic.ring2.horner_expr.add_const
3067
tactic.ring2.horner_expr.inv
3068
tactic.ring2.horner_expr.mul
3069
tactic.ring2.horner_expr.mul_aux
3070
tactic.ring2.horner_expr.mul_const
3071
tactic.ring2.horner_expr.neg
3072
tactic.ring2.horner_expr.pow
3073
tactic.ring2.horner_expr.to_string
3074
tactic.rintro
3075
tactic.rintro_hint
3076
tactic.rintro_parse
3077
tactic.root
3078
tactic.select
3079
tactic.split_if1
3080
tactic.split_ifs
3081
tactic.suggest.decl_data
3082
tactic.symm_eq
3083
tactic.symmetry_hyp
3084
tactic.tauto_state
3085
tactic.tautology
3086
tactic.tfae.arrow
3087
tactic.tfae.mk_implication
3088
tactic.tfae.mk_name
3089
tactic.tidy
3090
tactic.tidy.cfg
3091
tactic.tidy.core
3092
tactic.tidy.default_tactics
3093
tactic.tidy.ext1_wrapper
3094
tactic.tidy.name_to_tactic
3095
tactic.tidy.run_tactics
3096
tactic.tidy.tidy_attribute
3097
tactic.tidy_hole_cmd
3098
tactic.to_texpr
3099
tactic.trace_output
3100
tactic.trans_conv
3101
tactic.transfer
3102
tactic.transport_with_prefix_dict
3103
tactic.transport_with_prefix_fun
3104
tactic.try_intros
3105
tactic.unify_prefix
3106
tactic.unprime
3107
tactic.using_texpr
3108
tactic.valid_types
3109
tactic.wlog
3110
tensor_product
3111
tensor_product.assoc
3112
tensor_product.congr
3113
tensor_product.curry
3114
tensor_product.direct_sum
3115
tensor_product.lcurry
3116
tensor_product.lift
3117
tensor_product.lift.equiv
3118
tensor_product.lift_aux
3119
tensor_product.map
3120
tensor_product.mk
3121
tensor_product.relators
3122
tensor_product.smul.aux
3123
tensor_product.tmul
3124
tensor_product.uncurry
3125
times_cont_diff.times_cont_diff_fderiv_apply
3126
to_additive.attr
3127
to_additive.aux_attr
3128
to_additive.guess_name
3129
to_additive.map_namespace
3130
to_additive.parser
3131
to_additive.proceed_fields
3132
to_additive.target_name
3133
to_additive.tokens_dict
3134
to_additive.value_type
3135
topological_add_group.to_uniform_space
3136
topological_space.open_nhds
3137
topological_space.open_nhds.inclusion
3138
topological_space.open_nhds.inclusion_map_iso
3139
topological_space.open_nhds.map
3140
topological_space.opens.gi
3141
topological_space.opens.interior
3142
topological_space.opens.is_basis
3143
topological_space.opens.map_comp
3144
topological_space.opens.map_id
3145
topological_space.opens.map_iso
3146
topological_space.opens.to_Top
3147
topological_space.seq_tendsto_iff
3148
transfer.analyse_decls
3149
transfer.compute_transfer
3150
traversable
3151
traversable.fold_map
3152
traversable.foldl
3153
traversable.foldr
3154
traversable.free.map
3155
traversable.free.mk
3156
traversable.length
3157
traversable.map_fold
3158
traversable.mfoldl
3159
traversable.mfoldl.unop_of_free_monoid
3160
traversable.mfoldr
3161
traversable.pure_transformation
3162
tree
3163
tree.map
3164
tree.repr
3165
trunc.bind
3166
trunc.lift_on
3167
trunc.map
3168
trunc.rec
3169
trunc.rec_on
3170
trunc.rec_on_subsingleton
3171
turing.TM0.cfg.inhabited
3172
turing.TM0.cfg.map
3173
turing.TM0.machine
3174
turing.TM0.machine.map
3175
turing.TM0.machine.map_respects
3176
turing.TM0.machine.map_step
3177
turing.TM0.stmt.inhabited
3178
turing.TM0.stmt.map
3179
turing.TM0to1.tr
3180
turing.TM0to1.tr_cfg
3181
turing.TM0to1.Λ'
3182
turing.TM1.cfg.inhabited
3183
turing.TM1.eval
3184
turing.TM1.init
3185
turing.TM1.step
3186
turing.TM1.stmts
3187
turing.TM1.stmts₁
3188
turing.TM1.supports_stmt
3189
turing.TM1to0.tr
3190
turing.TM1to0.tr_aux
3191
turing.TM1to0.tr_cfg
3192
turing.TM1to0.tr_eval
3193
turing.TM1to0.tr_stmts
3194
turing.TM1to0.Λ'
3195
turing.TM1to1.move
3196
turing.TM1to1.read
3197
turing.TM1to1.read_aux
3198
turing.TM1to1.step_aux_move
3199
turing.TM1to1.step_aux_write
3200
turing.TM1to1.supports_stmt_move
3201
turing.TM1to1.supports_stmt_write
3202
turing.TM1to1.tr
3203
turing.TM1to1.tr_cfg
3204
turing.TM1to1.tr_normal
3205
turing.TM1to1.tr_supp
3206
turing.TM1to1.tr_tape
3207
turing.TM1to1.tr_tape'
3208
turing.TM1to1.tr_tape_drop_right
3209
turing.TM1to1.write
3210
turing.TM1to1.writes
3211
turing.TM1to1.Λ'
3212
turing.TM2.cfg
3213
turing.TM2.cfg.inhabited
3214
turing.TM2.eval
3215
turing.TM2.init
3216
turing.TM2.reaches
3217
turing.TM2.step
3218
turing.TM2.step_aux
3219
turing.TM2.stmts
3220
turing.TM2.stmts₁
3221
turing.TM2.supports
3222
turing.TM2.supports_stmt
3223
turing.TM2to1.st_act
3224
turing.TM2to1.st_run
3225
turing.TM2to1.st_var
3226
turing.TM2to1.st_write
3227
turing.TM2to1.stackel
3228
turing.TM2to1.stackel.get
3229
turing.TM2to1.stackel.is_bottom
3230
turing.TM2to1.stackel.is_top
3231
turing.TM2to1.stackel_equiv
3232
turing.TM2to1.stmt_st_rec
3233
turing.TM2to1.tr
3234
turing.TM2to1.tr_cfg
3235
turing.TM2to1.tr_init
3236
turing.TM2to1.tr_normal
3237
turing.TM2to1.tr_st_act
3238
turing.TM2to1.tr_stk
3239
turing.TM2to1.tr_stmts₁
3240
turing.TM2to1.tr_supp
3241
turing.TM2to1.Γ'
3242
turing.TM2to1.Λ'
3243
turing.dwrite
3244
turing.eval
3245
turing.frespects
3246
turing.pointed_map
3247
turing.reaches
3248
turing.reaches₀
3249
turing.reaches₁
3250
turing.respects
3251
turing.tape
3252
turing.tape.map
3253
turing.tape.mk
3254
turing.tape.mk'
3255
turing.tape.move
3256
turing.tape.nth
3257
turing.tape.write
3258
uniform_continuous
3259
uniform_continuous₂
3260
uniform_embedding
3261
uniform_inducing
3262
uniform_space.completion.completion_separation_quotient_equiv
3263
uniform_space.completion.cpkg
3264
uniform_space.completion.extension₂
3265
uniform_space.completion.map₂
3266
uniform_space.core.mk'
3267
uniform_space.mk'
3268
uniform_space.of_core
3269
uniform_space.of_core_eq
3270
uniform_space.sep_quot_equiv_ring_quot
3271
uniform_space.separation_quotient
3272
uniform_space.separation_quotient.lift
3273
uniform_space.separation_quotient.map
3274
uniform_space.separation_setoid
3275
uniformity_dist_of_mem_uniformity
3276
uniformity_edist
3277
uniformity_edist'
3278
uniformity_edist''
3279
uniformity_edist_nnreal
3280
unique
3281
unique.of_surjective
3282
unique_factorization_domain.exists_mem_factors_of_dvd
3283
unique_factorization_domain.of_unique_irreducible_factorization
3284
unique_irreducible_factorization
3285
unique_unique_equiv
3286
units
3287
units.inv'
3288
units.map
3289
units.map_equiv
3290
units.mk_of_mul_eq_one
3291
units.mul
3292
vector.insert_nth
3293
vector.m_of_fn
3294
vector.mmap
3295
vector.reverse
3296
vector.to_array
3297
vector.traverse
3298
vector.traverse_def
3299
vector3.cons_elim
3300
vector3.nil_elim
3301
vector3.rec_on
3302
vector_space.dim
3303
well_founded.succ
3304
well_founded.sup
3305
well_founded_submodule_gt
3306
where.binder_less_important
3307
where.binder_priority
3308
where.collect_by
3309
where.collect_by_aux
3310
where.collect_implicit_names
3311
where.compile_variable_list
3312
where.fetch_potential_variable_names
3313
where.find_var
3314
where.format_variable
3315
where.get_all_in_namespace
3316
where.get_def_variables
3317
where.get_includes_core
3318
where.get_namespace_core
3319
where.get_opens
3320
where.get_variables_core
3321
where.inflate
3322
where.is_in_namespace_nonsynthetic
3323
where.is_variable_name
3324
where.mk_flag
3325
where.resolve_var
3326
where.resolve_vars
3327
where.resolve_vars_aux
3328
where.select_for_which
3329
where.sort_variable_list
3330
where.strip_namespace
3331
where.strip_pi_binders
3332
where.strip_pi_binders_aux
3333
where.trace_end
3334
where.trace_includes
3335
where.trace_namespace
3336
where.trace_nl
3337
where.trace_opens
3338
where.trace_variables
3339
where.trace_where
3340
where.where_cmd
3341
with_bot
3342
with_one
3343
with_one.lift
3344
with_one.map
3345
with_top
3346
with_top.canonically_ordered_comm_semiring
3347
with_top.coe_eq_zero
3348
with_top.coe_zero
3349
with_top.has_one
3350
with_top.top_ne_zero
3351
with_top.zero_ne_top
3352
with_zero
3353
with_zero.div
3354
with_zero.inv
3355
with_zero.lift
3356
with_zero.map
3357
with_zero.ordered_comm_monoid
3358
writer
3359
writer_t
3360
writer_t.adapt
3361
writer_t.bind
3362
writer_t.call_cc
3363
writer_t.ext
3364
writer_t.lift
3365
writer_t.listen
3366
writer_t.mk_label
3367
writer_t.monad_cont
3368
writer_t.monad_except
3369
writer_t.monad_map
3370
writer_t.pass
3371
writer_t.pure
3372
writer_t.tell
3373
wseq.bisim_o
3374
wseq.cases_on
3375
wseq.destruct_append.aux
3376
wseq.destruct_join.aux
3377
wseq.drop.aux
3378
wseq.lift_rel_o
3379
wseq.mem
3380
wseq.tail.aux
3381
wseq.think_congr
3382
zmod
3383
zmod.cast
3384
zmod.to_module'
3385
zmod.units_equiv_coprime
3386
zmodp
3387
zmodp.legendre_sym
3388
znum.abs
3389
znum.add
3390
znum.bit0
3391
znum.bit1
3392
znum.bitm1
3393
znum.cmp
3394
znum.cmp_to_int
3395
znum.div
3396
znum.gcd
3397
znum.mod
3398
znum.mul
3399
znum.of_int'
3400
znum.pred
3401
znum.succ
3402
znum.transfer
3403
znum.transfer_rw
3404
znum.zneg
3405
zsqrtd.le
3406
zsqrtd.lt
3407
zsqrtd.norm
3408

3409
Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

Product

Resources

Company

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more, all in one place.

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.
