Skip to content

mathlib4 port status

Jump to bottom
Johan Commelin edited this page Mar 23, 2023 · 2862 revisions
Clone this wiki locally

Do not edit this file.

If you want to add free-form comments about files that don't have PRs yet,

edit https://github.com/leanprover-community/mathlib4/wiki/port-comments/_edit instead.

algebra.abs: Yes mathlib4#477 c4658a649d216f57e99621708b09dcb3dcccbd23
algebra.add_torsor: Yes mathlib4#1542 9003f28797c0664a49e4179487267c494477d853 blocked
  by dangerous instances
algebra.algebra.basic: Yes mathlib4#2244 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
algebra.algebra.bilinear: Yes mathlib4#2552 657df4339ae6ceada048c8a2980fb10e393143ec
algebra.algebra.equiv: Yes mathlib4#2413 bd9851ca476957ea4549eb19b40e7b5ade9428cc
algebra.algebra.hom: Yes mathlib4#2371 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
algebra.algebra.operations: Yes mathlib4#2568 27b54c47c3137250a521aa64e9f1db90be5f6a26
algebra.algebra.pi: Yes mathlib4#2549 b16045e4bf61c6fd619a1a68854ab3d605dcd017
algebra.algebra.prod: Yes mathlib4#2383 28aa996fc6fb4317f0083c4e6daf79878d81be33
algebra.algebra.restrict_scalars: Yes mathlib4#2563 c310cfdc40da4d99a10a58c33a95360ef9e6e0bf
algebra.algebra.spectrum: 'No'
algebra.algebra.subalgebra.basic: Yes mathlib4#2743 c4658a649d216f57e99621708b09dcb3dcccbd23
algebra.algebra.subalgebra.pointwise: Yes mathlib4#2913 b2c707cd190a58ea0565c86695a19e99ccecc215
algebra.algebra.subalgebra.tower: Yes mathlib4#2790 a35ddf20601f85f78cd57e7f5b09ed528d71b7af
algebra.algebra.tower: Yes mathlib4#2548 71150516f28d9826c7341f8815b31f7d8770c212
algebra.algebra.unitization: Yes mathlib4#2892 8f66240cab125b938b327d3850169d490cfbcdd8
algebra.algebraic_card: 'No'
algebra.associated: Yes mathlib4#1098 2f3994e1b117b1e1da49bcfb67334f33460c3ce4
algebra.big_operators.associated: Yes mathlib4#1943 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
algebra.big_operators.basic: Yes mathlib4#1628 6c5f73fd6f6cc83122788a80a27cdd54663609f4
algebra.big_operators.fin: Yes mathlib4#1848 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
algebra.big_operators.finprod: Yes mathlib4#1766 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
algebra.big_operators.finsupp: Yes mathlib4#1900 842328d9df7e96fd90fc424e115679c15fb23a71
algebra.big_operators.intervals: Yes mathlib4#1901 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
algebra.big_operators.multiset.basic: Yes mathlib4#1526 6c5f73fd6f6cc83122788a80a27cdd54663609f4
algebra.big_operators.multiset.lemmas: Yes mathlib4#1536 0a0ec35061ed9960bf0e7ffb0335f44447b58977
algebra.big_operators.nat_antidiagonal: Yes mathlib4#1656 008205aa645b3f194c1da47025c5f110c8406eab
algebra.big_operators.norm_num: 'No'
algebra.big_operators.option: Yes mathlib4#1653 008205aa645b3f194c1da47025c5f110c8406eab
algebra.big_operators.order: Yes mathlib4#1673 824f9ae93a4f5174d2ea948e2d75843dd83447bb
algebra.big_operators.pi: Yes mathlib4#1687 509de852e1de55e1efa8eacfa11df0823f26f226
algebra.big_operators.ring: Yes mathlib4#1645 008205aa645b3f194c1da47025c5f110c8406eab
algebra.big_operators.ring_equiv: Yes mathlib4#1647 008205aa645b3f194c1da47025c5f110c8406eab
algebra.bounds: Yes mathlib4#1452 dd71334db81d0bd444af1ee339a29298bef40734
algebra.category.Algebra.basic: 'No'
algebra.category.Algebra.limits: 'No'
algebra.category.BoolRing: 'No'
algebra.category.Group.Z_Module_equivalence: 'No'
algebra.category.Group.abelian: 'No'
algebra.category.Group.adjunctions: 'No'
algebra.category.Group.basic: No mathlib4#3036 524793de15bc4c52ee32d254e7d7867c7176b3af
algebra.category.Group.biproducts: 'No'
algebra.category.Group.colimits: 'No'
algebra.category.Group.epi_mono: 'No'
algebra.category.Group.equivalence_Group_AddGroup: 'No'
algebra.category.Group.filtered_colimits: 'No'
algebra.category.Group.images: 'No'
algebra.category.Group.injective: 'No'
algebra.category.Group.limits: 'No'
algebra.category.Group.preadditive: 'No'
algebra.category.Group.subobject: 'No'
algebra.category.Group.zero: 'No'
algebra.category.GroupWithZero: 'No'
algebra.category.Module.abelian: 'No'
algebra.category.Module.adjunctions: 'No'
algebra.category.Module.algebra: 'No'
algebra.category.Module.basic: 'No'
algebra.category.Module.biproducts: 'No'
algebra.category.Module.change_of_rings: 'No'
algebra.category.Module.colimits: 'No'
algebra.category.Module.epi_mono: 'No'
algebra.category.Module.filtered_colimits: 'No'
algebra.category.Module.images: 'No'
algebra.category.Module.kernels: 'No'
algebra.category.Module.limits: 'No'
algebra.category.Module.monoidal: 'No'
algebra.category.Module.products: 'No'
algebra.category.Module.projective: 'No'
algebra.category.Module.simple: 'No'
algebra.category.Module.subobject: 'No'
algebra.category.Module.tannaka: 'No'
algebra.category.Mon.adjunctions: 'No'
algebra.category.Mon.basic: Yes mathlib4#2902 4125b9adf2e268d1cf438092d690a78f7c664743
algebra.category.Mon.colimits: 'No'
algebra.category.Mon.filtered_colimits: 'No'
algebra.category.Mon.limits: 'No'
algebra.category.Ring.adjunctions: 'No'
algebra.category.Ring.basic: 'No'
algebra.category.Ring.colimits: 'No'
algebra.category.Ring.constructions: 'No'
algebra.category.Ring.filtered_colimits: 'No'
algebra.category.Ring.instances: 'No'
algebra.category.Ring.limits: 'No'
algebra.category.Semigroup.basic: 'No'
algebra.category.fgModule.basic: 'No'
algebra.category.fgModule.limits: 'No'
algebra.char_p.algebra: Yes mathlib4#3037 96782a2d6dcded92116d8ac9ae48efb41d46a27c
algebra.char_p.basic: Yes mathlib4#2845 05a78c9451101108e638a0f213fb1bed82483545
algebra.char_p.char_and_card: 'No'
algebra.char_p.exp_char: Yes mathlib4#2894 70fd9563a21e7b963887c9360bd29b2393e6225a
algebra.char_p.invertible: Yes mathlib4#2855 70fd9563a21e7b963887c9360bd29b2393e6225a
algebra.char_p.local_ring: 'No'
algebra.char_p.mixed_char_zero: 'No'
algebra.char_p.pi: Yes mathlib4#2874 168ad7fc5d8173ad38be9767a22d50b8ecf1cd00
algebra.char_p.quotient: 'No'
algebra.char_p.subring: Yes mathlib4#2876 168ad7fc5d8173ad38be9767a22d50b8ecf1cd00
algebra.char_p.two: Yes mathlib4#2873 7f1ba1a333d66eed531ecb4092493cd1b6715450
algebra.char_zero.defs: Yes mathlib4#661 d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
algebra.char_zero.infinite: Yes mathlib4#1694 0a0ec35061ed9960bf0e7ffb0335f44447b58977
algebra.char_zero.lemmas: Yes mathlib4#1164 acee671f47b8e7972a1eb6f4eed74b4b3abce829
algebra.char_zero.quotient: Yes mathlib4#2022 d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
algebra.continued_fractions.basic: 'No'
algebra.continued_fractions.computation.approximation_corollaries: 'No'
algebra.continued_fractions.computation.approximations: 'No'
algebra.continued_fractions.computation.basic: 'No'
algebra.continued_fractions.computation.correctness_terminating: 'No'
algebra.continued_fractions.computation.terminates_iff_rat: 'No'
algebra.continued_fractions.computation.translations: 'No'
algebra.continued_fractions.continuants_recurrence: 'No'
algebra.continued_fractions.convergents_equiv: 'No'
algebra.continued_fractions.terminated_stable: 'No'
algebra.continued_fractions.translations: 'No'
algebra.covariant_and_contravariant: Yes mathlib4#467 2258b40dacd2942571c8ce136215350c702dc78f
algebra.cubic_discriminant: 'No'
algebra.direct_limit: 'No'
algebra.direct_sum.algebra: 'No'
algebra.direct_sum.basic: Yes mathlib4#1923 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
algebra.direct_sum.decomposition: No mathlib4#3001 4e861f25ba5ceef42ba0712d8ffeb32f38ad6441
algebra.direct_sum.finsupp: Yes mathlib4#2995 aca0874a9ce95510752f4075f80f273172e9b177
algebra.direct_sum.internal: 'No'
algebra.direct_sum.module: Yes mathlib4#2596 6623e6af705e97002a9054c1c05a980180276fc1
algebra.direct_sum.ring: No mathlib4#1968 861a26926586cd46ff80264d121cdb6fa0e35cc1
algebra.divisibility.basic: Yes mathlib4#833 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.divisibility.units: Yes mathlib4#848 e574b1a4e891376b0ef974b926da39e05da12a06
algebra.dual_number: Yes mathlib4#2987 b8d2eaa69d69ce8f03179a5cda774fc0cde984e4
algebra.dual_quaternion: 'No'
algebra.euclidean_domain.basic: Yes mathlib4#919 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.euclidean_domain.defs: Yes mathlib4#871 f1a2caaf51ef593799107fe9a8d5e411599f3996
algebra.euclidean_domain.instances: Yes mathlib4#959 e1bccd6e40ae78370f01659715d3c948716e3b7e
algebra.field.basic: Yes mathlib4#975 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
algebra.field.defs: Yes mathlib4#668 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.field.opposite: Yes mathlib4#1049 aba57d4d3dae35460225919dcd82fe91355162f9
algebra.field.power: Yes mathlib4#1305 1e05171a5e8cf18d98d9cf7b207540acb044acae
algebra.field.ulift: Yes mathlib4#2911 13e18cfa070ea337ea960176414f5ae3a1534aae
algebra.free: Yes mathlib4#1353 6d0adfa76594f304b4650d098273d4366edeb61b
algebra.free_algebra: Yes mathlib4#2905 6623e6af705e97002a9054c1c05a980180276fc1
algebra.free_monoid.basic: Yes mathlib4#1443 657df4339ae6ceada048c8a2980fb10e393143ec
algebra.free_monoid.count: Yes mathlib4#1483 a2d2e18906e2b62627646b5d5be856e6a642062f
algebra.free_non_unital_non_assoc_algebra: Yes mathlib4#2642 2f1a4aff21c9aadf7cfb96911734754d6c228029
algebra.gcd_monoid.basic: Yes mathlib4#1135 550b58538991c8977703fdeb7c9d51a5aa27df11
algebra.gcd_monoid.div: 'No'
algebra.gcd_monoid.finset: Yes mathlib4#1612 9003f28797c0664a49e4179487267c494477d853
algebra.gcd_monoid.integrally_closed: 'No'
algebra.gcd_monoid.multiset: Yes mathlib4#1565 f694c7dead66f5d4c80f446c796a5aad14707f0e
algebra.geom_sum: Yes mathlib4#1922 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
algebra.graded_monoid: Yes mathlib4#1689 008205aa645b3f194c1da47025c5f110c8406eab
algebra.graded_mul_action: Yes mathlib4#1959 861a26926586cd46ff80264d121cdb6fa0e35cc1
algebra.group.basic: Yes mathlib4#4 2196ab363eb097c008d4497125e0dde23fb36db2
algebra.group.commutator: Yes mathlib4#582 c4658a649d216f57e99621708b09dcb3dcccbd23
algebra.group.commute: Yes mathlib4#457 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.group.conj: Yes mathlib4#1158 0743cc5d9d86bcd1bba10f480e948a257d65056f
algebra.group.conj_finite: Yes mathlib4#1737 1126441d6bccf98c81214a0780c73d499f6721fe
algebra.group.defs: Yes mathlib4#4 2e0975f6a25dd3fbfb9e41556a77f075f6269748
algebra.group.ext: Yes mathlib4#850 e574b1a4e891376b0ef974b926da39e05da12a06
algebra.group.inj_surj: Yes mathlib4#707 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
algebra.group.opposite: Yes mathlib4#912 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.group.order_synonym: Yes mathlib4#651 d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
algebra.group.pi: Yes mathlib4#1088 b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7
algebra.group.prod: Yes mathlib4#968 cf9386b56953fb40904843af98b7a80757bbe7f9
algebra.group.semiconj: Yes mathlib4#457 a148d797a1094ab554ad4183a4ad6f130358ef64
algebra.group.type_tags: Yes mathlib4#832 2e0975f6a25dd3fbfb9e41556a77f075f6269748
algebra.group.ulift: Yes mathlib4#906 13e18cfa070ea337ea960176414f5ae3a1534aae
algebra.group.unique_prods: Yes mathlib4#1764 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
algebra.group.units: Yes mathlib4#457 369525b73f229ccd76a6ec0e0e0bf2be57599768
algebra.group.with_one.basic: Yes mathlib4#922 4dc134b97a3de65ef2ed881f3513d56260971562
algebra.group.with_one.defs: Yes mathlib4#841 995b47e555f1b6297c7cf16855f1023e355219fb
algebra.group.with_one.units: Yes mathlib4#955 4e87c8477c6c38b753f050bc9664b94ee859896c
algebra.group_power.basic: Yes mathlib4#457 9b2660e1b25419042c8da10bf411aa3c67f14383
algebra.group_power.identities: Yes mathlib4#531 c4658a649d216f57e99621708b09dcb3dcccbd23
algebra.group_power.lemmas: Yes mathlib4#507 e1bccd6e40ae78370f01659715d3c948716e3b7e
algebra.group_power.order: Yes mathlib4#1043 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
algebra.group_power.ring: Yes mathlib4#979 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
algebra.group_ring_action.basic: Yes _ 207cfac9fcd06138865b5d04f7091e46d9320432
algebra.group_ring_action.invariant: Yes mathlib4#2970 e7bab9a85e92cf46c02cb4725a7be2f04691e3a7
algebra.group_ring_action.subobjects: Yes mathlib4#1849 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
algebra.group_with_zero.basic: Yes mathlib4#669 2196ab363eb097c008d4497125e0dde23fb36db2
algebra.group_with_zero.commute: Yes mathlib4#762 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.group_with_zero.defs: Yes mathlib4#4 2f3994e1b117b1e1da49bcfb67334f33460c3ce4
algebra.group_with_zero.divisibility: Yes mathlib4#870 f1a2caaf51ef593799107fe9a8d5e411599f3996
algebra.group_with_zero.inj_surj: Yes mathlib4#722 a148d797a1094ab554ad4183a4ad6f130358ef64
algebra.group_with_zero.power: Yes mathlib4#1251 46a64b5b4268c594af770c44d9e502afc6a515cb
algebra.group_with_zero.semiconj: Yes mathlib4#757 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.group_with_zero.units.basic: Yes mathlib4#735 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.group_with_zero.units.lemmas: Yes mathlib4#920 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
algebra.hierarchy_design: Yes mathlib4#657 41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3
algebra.hom.aut: Yes mathlib4#1111 d4f69d96f3532729da8ebb763f4bc26fcf640f06
algebra.hom.centroid: Yes mathlib4#1325 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
algebra.hom.commute: Yes mathlib4#831 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904
algebra.hom.embedding: Yes mathlib4#764 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.hom.equiv.basic: Yes mathlib4#835 67f362670ed961bcb80239dc40ca18bcd4289c77
algebra.hom.equiv.type_tags: Yes mathlib4#943 3342d1b2178381196f818146ff79bc0e7ccd9e2d
algebra.hom.equiv.units.basic: Yes mathlib4#895 a95b16cbade0f938fc24abd05412bde1e84bab9b
algebra.hom.equiv.units.group_with_zero: Yes mathlib4#901 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.hom.freiman: Yes mathlib4#1538 f694c7dead66f5d4c80f446c796a5aad14707f0e
algebra.hom.group: Yes mathlib4#659 8c53048add6ffacdda0b36c4917bfe37e209b0ba
algebra.hom.group_action: Yes mathlib4#1424 e7bab9a85e92cf46c02cb4725a7be2f04691e3a7
algebra.hom.group_instances: Yes mathlib4#941 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
algebra.hom.iterate: Yes mathlib4#1133 792a2a264169d64986541c6f8f7e3bbb6acb6295
algebra.hom.non_unital_alg: Yes mathlib4#2414 bd9851ca476957ea4549eb19b40e7b5ade9428cc
algebra.hom.ring: Yes mathlib4#958 cf9386b56953fb40904843af98b7a80757bbe7f9
algebra.hom.units: Yes mathlib4#745 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
algebra.homology.Module: 'No'
algebra.homology.additive: 'No'
algebra.homology.augment: 'No'
algebra.homology.complex_shape: Yes mathlib4#635 c4658a649d216f57e99621708b09dcb3dcccbd23
algebra.homology.differential_object: 'No'
algebra.homology.exact: 'No'
algebra.homology.flip: 'No'
algebra.homology.functor: 'No'
algebra.homology.homological_complex: 'No'
algebra.homology.homology: 'No'
algebra.homology.homotopy: 'No'
algebra.homology.homotopy_category: 'No'
algebra.homology.image_to_kernel: 'No'
algebra.homology.opposite: 'No'
algebra.homology.quasi_iso: 'No'
algebra.homology.short_exact.abelian: 'No'
algebra.homology.short_exact.preadditive: 'No'
algebra.homology.single: 'No'
algebra.indicator_function: Yes mathlib4#1752 2445c98ae4b87eabebdde552593519b9b6dc350c
algebra.invertible: Yes mathlib4#930 10b4e499f43088dd3bb7b5796184ad5216648ab1
algebra.is_prime_pow: Yes mathlib4#1925 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
algebra.jordan.basic: 'No'
algebra.lie.abelian: 'No'
algebra.lie.base_change: 'No'
algebra.lie.basic: Yes mathlib4#2262 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
algebra.lie.cartan_matrix: 'No'
algebra.lie.cartan_subalgebra: 'No'
algebra.lie.character: 'No'
algebra.lie.classical: 'No'
algebra.lie.direct_sum: 'No'
algebra.lie.engel: 'No'
algebra.lie.free: 'No'
algebra.lie.ideal_operations: 'No'
algebra.lie.matrix: 'No'
algebra.lie.nilpotent: 'No'
algebra.lie.non_unital_non_assoc_algebra: Yes mathlib4#2602 841ac1a3d9162bf51c6327812ecb6e5e71883ac4
algebra.lie.normalizer: 'No'
algebra.lie.of_associative: 'No'
algebra.lie.quotient: 'No'
algebra.lie.semisimple: 'No'
algebra.lie.skew_adjoint: 'No'
algebra.lie.solvable: 'No'
algebra.lie.subalgebra: Yes mathlib4#3016 6d584f1709bedbed9175bd9350df46599bdd7213
algebra.lie.submodule: No mathlib4#3045 9822b65bfc4ac74537d77ae318d27df1df662471
algebra.lie.tensor_product: 'No'
algebra.lie.universal_enveloping: 'No'
algebra.lie.weights: 'No'
algebra.linear_recurrence: 'No'
algebra.module.algebra: Yes mathlib4#2370 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
algebra.module.basic: Yes mathlib4#1169 966e0cf0685c9cedf8a3283ac69eef4d5f2eaca2
algebra.module.big_operators: Yes mathlib4#1665 509de852e1de55e1efa8eacfa11df0823f26f226
algebra.module.bimodule: 'No'
algebra.module.dedekind_domain: 'No'
algebra.module.equiv: Yes mathlib4#1732 ea94d7cd54ad9ca6b7710032868abb7c6a104c9c
algebra.module.graded_module: 'No'
algebra.module.hom: Yes mathlib4#1417 134625f523e737f650a6ea7f0c82a6177e45e622
algebra.module.injective: 'No'
algebra.module.linear_map: Yes mathlib4#1587 cc8e88c7c8c7bc80f91f84d11adb584bf9bd658f
algebra.module.localized_module: No please wait for mathlib3#17973
algebra.module.opposites: Yes mathlib4#1879 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
algebra.module.pi: Yes mathlib4#1283 a437a2499163d85d670479f69f625f461cc5fef9
algebra.module.pid: 'No'
algebra.module.pointwise_pi: Yes mathlib4#1557 9003f28797c0664a49e4179487267c494477d853
algebra.module.prod: Yes mathlib4#1282 a437a2499163d85d670479f69f625f461cc5fef9
algebra.module.projective: 'No'
algebra.module.submodule.basic: Yes mathlib4#1888 feb99064803fd3108e37c18b0f77d0a8344677a3
algebra.module.submodule.bilinear: Yes mathlib4#2531 6010cf523816335f7bae7f8584cb2edaace73940
algebra.module.submodule.lattice: Yes mathlib4#1898 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
algebra.module.submodule.pointwise: Yes mathlib4#2285 48085f140e684306f9e7da907cd5932056d1aded
algebra.module.torsion: No please wait for mathlib3#14734
algebra.module.ulift: Yes mathlib4#1880 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
algebra.monoid_algebra.basic: Yes mathlib4#2589 6623e6af705e97002a9054c1c05a980180276fc1
algebra.monoid_algebra.degree: Yes mathlib4#2918 f694c7dead66f5d4c80f446c796a5aad14707f0e
algebra.monoid_algebra.division: No please wait for mathlib3#18633 to be through mathport
algebra.monoid_algebra.grading: 'No'
algebra.monoid_algebra.no_zero_divisors: Yes mathlib4#2938 3e067975886cf5801e597925328c335609511b1a
algebra.monoid_algebra.support: Yes mathlib4#2720 16749fc4661828cba18cd0f4e3c5eb66a8e80598
algebra.monoid_algebra.to_direct_sum: 'No'
algebra.ne_zero: Yes mathlib4#557 f340f229b1f461aa1c8ee11e0a172d0a3b301a4a
algebra.opposites: Yes mathlib4#644 7a89b1aed52bcacbcc4a8ad515e72c5c07268940
algebra.order.absolute_value: Yes mathlib4#974 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
algebra.order.algebra: Yes mathlib4#2535 f5a600f8102c8bfdbd22781968a20a539304c1b4
algebra.order.archimedean: Yes mathlib4#1462 6f413f3f7330b94c92a5a27488fdc74e6d483a78
algebra.order.chebyshev: 'No'
algebra.order.complete_field: 'No'
algebra.order.euclidean_absolute_value: Yes mathlib4#1267 422e70f7ce183d2900c586a8cda8381e788a0c62
algebra.order.field.basic: Yes mathlib4#1065 5a82b0671532663333e205f422124a98bdfe673f
algebra.order.field.canonical.basic: Yes mathlib4#1018 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
algebra.order.field.canonical.defs: Yes mathlib4#985 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
algebra.order.field.defs: Yes mathlib4#905 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.order.field.inj_surj: Yes mathlib4#1017 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
algebra.order.field.pi: Yes mathlib4#1695 509de852e1de55e1efa8eacfa11df0823f26f226
algebra.order.field.power: Yes mathlib4#1256 422e70f7ce183d2900c586a8cda8381e788a0c62
algebra.order.floor: Yes mathlib4#1304 afdb43429311b885a7988ea15d0bac2aac80f69c
algebra.order.group.abs: Yes mathlib4#896 2196ab363eb097c008d4497125e0dde23fb36db2
algebra.order.group.bounds: Yes mathlib4#1069 d012cd09a9b256d870751284dd6a29882b0be105
algebra.order.group.defs: Yes mathlib4#869 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
algebra.order.group.densely_ordered: Yes mathlib4#956 4e87c8477c6c38b753f050bc9664b94ee859896c
algebra.order.group.inj_surj: Yes mathlib4#916 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.order.group.instances: Yes mathlib4#890 55bbb8076236154a4f53939a62ad1e4fddbc14c8
algebra.order.group.min_max: Yes mathlib4#933 10b4e499f43088dd3bb7b5796184ad5216648ab1
algebra.order.group.order_iso: Yes mathlib4#895 a95b16cbade0f938fc24abd05412bde1e84bab9b
algebra.order.group.prod: Yes mathlib4#1026 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
algebra.order.group.type_tags: Yes mathlib4#921 2258b40dacd2942571c8ce136215350c702dc78f
algebra.order.group.units: Yes mathlib4#898 a95b16cbade0f938fc24abd05412bde1e84bab9b
algebra.order.group.with_top: Yes mathlib4#946 f178c0e25af359f6cbc72a96a243efd3b12423a3
algebra.order.hom.basic: Yes mathlib4#627 28aa996fc6fb4317f0083c4e6daf79878d81be33
algebra.order.hom.monoid: Yes mathlib4#944 3342d1b2178381196f818146ff79bc0e7ccd9e2d
algebra.order.hom.ring: Yes mathlib4#1482 a2d2e18906e2b62627646b5d5be856e6a642062f
algebra.order.interval: 'No'
algebra.order.invertible: Yes mathlib4#1006 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
algebra.order.kleene: Yes mathlib4#2164 98e83c3d541c77cdb7da20d79611a780ff8e7d90
algebra.order.lattice_group: Yes mathlib4#934 10b4e499f43088dd3bb7b5796184ad5216648ab1
algebra.order.module: Yes mathlib4#1573 9003f28797c0664a49e4179487267c494477d853
algebra.order.monoid.basic: Yes mathlib4#872 9b2660e1b25419042c8da10bf411aa3c67f14383
algebra.order.monoid.cancel.basic: Yes mathlib4#883 f1a2caaf51ef593799107fe9a8d5e411599f3996
algebra.order.monoid.cancel.defs: Yes mathlib4#774 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.order.monoid.canonical.defs: Yes mathlib4#778 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.order.monoid.defs: Yes mathlib4#771 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.order.monoid.lemmas: Yes mathlib4#608 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
algebra.order.monoid.min_max: Yes mathlib4#763 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.order.monoid.nat_cast: Yes mathlib4#893 07fee0ca54c320250c98bacf31ca5f288b2bcbe2
algebra.order.monoid.order_dual: Yes mathlib4#786 2258b40dacd2942571c8ce136215350c702dc78f
algebra.order.monoid.prod: Yes mathlib4#987 2258b40dacd2942571c8ce136215350c702dc78f
algebra.order.monoid.to_mul_bot: Yes mathlib4#1024 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
algebra.order.monoid.type_tags: Yes mathlib4#873 2258b40dacd2942571c8ce136215350c702dc78f
algebra.order.monoid.units: Yes mathlib4#873 f1a2caaf51ef593799107fe9a8d5e411599f3996
algebra.order.monoid.with_top: Yes mathlib4#902 0111834459f5d7400215223ea95ae38a1265a907
algebra.order.monoid.with_zero.basic: Yes mathlib4#851 dad7ecf9a1feae63e6e49f07619b7087403fb8d4
algebra.order.monoid.with_zero.defs: Yes mathlib4#851 4dc134b97a3de65ef2ed881f3513d56260971562
algebra.order.nonneg.field: Yes mathlib4#2200 b3f4f007a962e3787aa0f3b5c7942a1317f7d88e
algebra.order.nonneg.floor: Yes mathlib4#2911 b3f4f007a962e3787aa0f3b5c7942a1317f7d88e
algebra.order.nonneg.ring: Yes mathlib4#1260 422e70f7ce183d2900c586a8cda8381e788a0c62
  Blocked by difficult to diagnose timeout
algebra.order.pi: Yes mathlib4#1259 422e70f7ce183d2900c586a8cda8381e788a0c62
algebra.order.pointwise: Yes mathlib4#1533 9003f28797c0664a49e4179487267c494477d853
algebra.order.positive.field: Yes mathlib4#1129 bbeb185db4ccee8ed07dc48449414ebfa39cb821
algebra.order.positive.ring: Yes mathlib4#911 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.order.rearrangement: No mathlib4#2268 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
algebra.order.ring.abs: Yes mathlib4#929 10b4e499f43088dd3bb7b5796184ad5216648ab1
algebra.order.ring.canonical: Yes mathlib4#905 824f9ae93a4f5174d2ea948e2d75843dd83447bb
algebra.order.ring.char_zero: Yes mathlib4#905 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.order.ring.cone: Yes mathlib4#935 10b4e499f43088dd3bb7b5796184ad5216648ab1
algebra.order.ring.defs: Yes mathlib4#905 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.order.ring.inj_surj: Yes mathlib4#917 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.order.ring.lemmas: Yes mathlib4#482 c4658a649d216f57e99621708b09dcb3dcccbd23
algebra.order.ring.with_top: Yes mathlib4#976 0111834459f5d7400215223ea95ae38a1265a907
algebra.order.smul: Yes mathlib4#1553 9003f28797c0664a49e4179487267c494477d853
algebra.order.sub.basic: Yes mathlib4#936 10b4e499f43088dd3bb7b5796184ad5216648ab1
algebra.order.sub.canonical: Yes mathlib4#814 62a5626868683c104774de8d85b9855234ac807c
algebra.order.sub.defs: Yes mathlib4#732 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.order.sub.with_top: Yes mathlib4#932 afdb4fa3b32d41106a4a09b371ce549ad7958abd
algebra.order.to_interval_mod: No mathlib4#2148 0a0ec35061ed9960bf0e7ffb0335f44447b58977
  Would be nice to finish mathlib3#17743 first
algebra.order.upper_lower: Yes mathlib4#2008 d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
algebra.order.with_zero: Yes mathlib4#903 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.order.zero_le_one: Yes mathlib4#893 07fee0ca54c320250c98bacf31ca5f288b2bcbe2
algebra.parity: Yes mathlib4#1092 8631e2d5ea77f6c13054d9151d82b83069680cb1
algebra.pempty_instances: Yes mathlib4#615 c3019c79074b0619edb4b27553a91b2e82242395
algebra.periodic: Yes mathlib4#1963 2196ab363eb097c008d4497125e0dde23fb36db2
algebra.polynomial.big_operators: Yes mathlib4#2750 47adfab39a11a072db552f47594bf8ed2cf8a722
algebra.polynomial.group_ring_action: Yes mathlib4#2863 afad8e438d03f9d89da2914aa06cb4964ba87a18
algebra.punit_instances: Yes mathlib4#1319 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
algebra.quadratic_discriminant: Yes mathlib4#2964 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
algebra.quandle: Yes mathlib4#1817 28aa996fc6fb4317f0083c4e6daf79878d81be33
algebra.quaternion: No please wait for mathlib3#18349
algebra.quaternion_basis: 'No'
algebra.quotient: Yes mathlib4#643 d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
algebra.regular.basic: Yes mathlib4#758 5cd3c25312f210fec96ba1edb2aebfb2ccf2010f
algebra.regular.pow: Yes mathlib4#1248 46a64b5b4268c594af770c44d9e502afc6a515cb
algebra.regular.smul: Yes mathlib4#1154 550b58538991c8977703fdeb7c9d51a5aa27df11
algebra.ring.add_aut: Yes mathlib4#1284 a437a2499163d85d670479f69f625f461cc5fef9
algebra.ring.aut: Yes mathlib4#1228 207cfac9fcd06138865b5d04f7091e46d9320432
algebra.ring.basic: Yes mathlib4#4 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
algebra.ring.boolean_ring: No mathlib4#2104 4c19a16e4b705bf135cf9a80ac18fcc99c438514
algebra.ring.commute: Yes mathlib4#759 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.ring.comp_typeclasses: Yes mathlib4#1226 207cfac9fcd06138865b5d04f7091e46d9320432
algebra.ring.defs: Yes mathlib4#655 314d3a578607dbd2eb2481ab15fceeb62b36cbdb
algebra.ring.divisibility: Yes mathlib4#864 f1a2caaf51ef593799107fe9a8d5e411599f3996
algebra.ring.equiv: Yes mathlib4#1077 a59dad53320b73ef180174aae867addd707ef00e
algebra.ring.fin: Yes mathlib4#1800 1f0096e6caa61e9c849ec2adbd227e960e9dff58
algebra.ring.idempotents: Yes mathlib4#918 655994e298904d7e5bbd1e18c95defd7b543eb94
algebra.ring.inj_surj: Yes mathlib4#734 a148d797a1094ab554ad4183a4ad6f130358ef64
algebra.ring.opposite: Yes mathlib4#977 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
algebra.ring.order_synonym: Yes mathlib4#671 d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
algebra.ring.pi: Yes mathlib4#1151 ba2245edf0c8bb155f1569fd9b9492a9b384cde6
algebra.ring.prod: Yes mathlib4#1229 207cfac9fcd06138865b5d04f7091e46d9320432
algebra.ring.regular: Yes mathlib4#795 2f3994e1b117b1e1da49bcfb67334f33460c3ce4
algebra.ring.semiconj: Yes mathlib4#751 70d50ecfd4900dd6d328da39ab7ebd516abe4025
algebra.ring.ulift: Yes mathlib4#1240 13e18cfa070ea337ea960176414f5ae3a1534aae
algebra.ring.units: Yes mathlib4#746 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
algebra.ring_quot: No please wait for mathlib3#17892
algebra.smul_with_zero: Yes mathlib4#1183 966e0cf0685c9cedf8a3283ac69eef4d5f2eaca2
algebra.squarefree: Yes mathlib4#3018 79de90f7beca025f469dcda978ae655c4d985946
algebra.star.basic: Yes mathlib4#1331 44b58b42794e5abe2bf86397c38e26b587e07e59
algebra.star.big_operators: Yes mathlib4#1648 008205aa645b3f194c1da47025c5f110c8406eab
algebra.star.chsh: 'No'
algebra.star.free: No mathlib4#3007 07c3cf2d851866ff7198219ed3fedf42e901f25c
algebra.star.module: Yes mathlib4#2441 09d7fe375d1f63d17cf6b2aa4b413ab3e6ec49df
algebra.star.pi: Yes mathlib4#1432 247a102b14f3cebfee126293341af5f6bed00237
algebra.star.pointwise: Yes mathlib4#1749 2445c98ae4b87eabebdde552593519b9b6dc350c
algebra.star.prod: Yes mathlib4#1434 247a102b14f3cebfee126293341af5f6bed00237
algebra.star.self_adjoint: Yes mathlib4#1860 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
algebra.star.star_alg_hom: Yes mathlib4#2603 35882ddc66524b6980532a123a4ad4166db34c81
algebra.star.subalgebra: Yes mathlib4#2819 160ef3e338a2a4f21a280e4c152d4016156e516d
algebra.star.unitary: Yes mathlib4#1436 247a102b14f3cebfee126293341af5f6bed00237
algebra.support: Yes mathlib4#1747 2445c98ae4b87eabebdde552593519b9b6dc350c
algebra.symmetrized: 'No'
algebra.triv_sq_zero_ext: Yes mathlib4#2951 ce7e9d53d4bbc38065db3b595cd5bd73c323bc1d
algebra.tropical.basic: Yes mathlib4#1165 9116dd6709f303dcf781632e15fdef382b0fc579
algebra.tropical.big_operators: Yes mathlib4#1760 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
algebra.tropical.lattice: Yes mathlib4#1349 6d0adfa76594f304b4650d098273d4366edeb61b
algebraic_geometry.AffineScheme: 'No'
algebraic_geometry.Gamma_Spec_adjunction: 'No'
algebraic_geometry.Scheme: 'No'
algebraic_geometry.Spec: 'No'
algebraic_geometry.elliptic_curve.point: 'No'
algebraic_geometry.elliptic_curve.weierstrass: 'No'
algebraic_geometry.function_field: 'No'
algebraic_geometry.gluing: 'No'
algebraic_geometry.limits: 'No'
algebraic_geometry.locally_ringed_space: 'No'
algebraic_geometry.locally_ringed_space.has_colimits: 'No'
algebraic_geometry.morphisms.basic: 'No'
algebraic_geometry.morphisms.finite_type: 'No'
algebraic_geometry.morphisms.open_immersion: 'No'
algebraic_geometry.morphisms.quasi_compact: 'No'
algebraic_geometry.morphisms.quasi_separated: 'No'
algebraic_geometry.morphisms.ring_hom_properties: 'No'
algebraic_geometry.morphisms.universally_closed: 'No'
algebraic_geometry.open_immersion: 'No'
algebraic_geometry.presheafed_space: 'No'
algebraic_geometry.presheafed_space.gluing: 'No'
algebraic_geometry.presheafed_space.has_colimits: 'No'
algebraic_geometry.prime_spectrum.basic: 'No'
algebraic_geometry.prime_spectrum.is_open_comap_C: 'No'
algebraic_geometry.prime_spectrum.maximal: 'No'
algebraic_geometry.prime_spectrum.noetherian: 'No'
algebraic_geometry.projective_spectrum.scheme: 'No'
algebraic_geometry.projective_spectrum.structure_sheaf: 'No'
algebraic_geometry.projective_spectrum.topology: 'No'
algebraic_geometry.properties: 'No'
algebraic_geometry.pullbacks: 'No'
algebraic_geometry.ringed_space: 'No'
algebraic_geometry.sheafed_space: 'No'
algebraic_geometry.stalks: 'No'
algebraic_geometry.structure_sheaf: 'No'
algebraic_topology.Moore_complex: 'No'
algebraic_topology.alternating_face_map_complex: 'No'
algebraic_topology.cech_nerve: 'No'
algebraic_topology.dold_kan.decomposition: 'No'
algebraic_topology.dold_kan.degeneracies: 'No'
algebraic_topology.dold_kan.equivalence_additive: 'No'
algebraic_topology.dold_kan.faces: 'No'
algebraic_topology.dold_kan.functor_gamma: 'No'
algebraic_topology.dold_kan.functor_n: 'No'
algebraic_topology.dold_kan.gamma_comp_n: 'No'
algebraic_topology.dold_kan.homotopies: 'No'
algebraic_topology.dold_kan.homotopy_equivalence: 'No'
algebraic_topology.dold_kan.n_comp_gamma: 'No'
algebraic_topology.dold_kan.n_reflects_iso: 'No'
algebraic_topology.dold_kan.normalized: 'No'
algebraic_topology.dold_kan.notations: 'No'
algebraic_topology.dold_kan.p_infty: 'No'
algebraic_topology.dold_kan.projections: 'No'
algebraic_topology.dold_kan.split_simplicial_object: 'No'
algebraic_topology.extra_degeneracy: 'No'
algebraic_topology.fundamental_groupoid.basic: 'No'
algebraic_topology.fundamental_groupoid.fundamental_group: 'No'
algebraic_topology.fundamental_groupoid.induced_maps: 'No'
algebraic_topology.fundamental_groupoid.product: 'No'
algebraic_topology.fundamental_groupoid.punit: 'No'
algebraic_topology.fundamental_groupoid.simply_connected: 'No'
algebraic_topology.nerve: 'No'
algebraic_topology.simplex_category: 'No'
algebraic_topology.simplicial_object: 'No'
algebraic_topology.simplicial_set: 'No'
algebraic_topology.split_simplicial_object: 'No'
algebraic_topology.topological_simplex: 'No'
analysis.ODE.gronwall: 'No'
analysis.ODE.picard_lindelof: 'No'
analysis.analytic.basic: 'No'
analysis.analytic.composition: 'No'
analysis.analytic.inverse: 'No'
analysis.analytic.isolated_zeros: 'No'
analysis.analytic.linear: 'No'
analysis.analytic.radius_liminf: 'No'
analysis.analytic.uniqueness: 'No'
analysis.asymptotics.asymptotic_equivalent: 'No'
analysis.asymptotics.asymptotics: 'No'
analysis.asymptotics.specific_asymptotics: 'No'
analysis.asymptotics.superpolynomial_decay: 'No'
analysis.asymptotics.theta: 'No'
analysis.bounded_variation: 'No'
analysis.box_integral.basic: 'No'
analysis.box_integral.box.basic: No mathlib4#2625 f2ce6086713c78a7f880485f7917ea547a215982
analysis.box_integral.box.subbox_induction: 'No'
analysis.box_integral.divergence_theorem: 'No'
analysis.box_integral.integrability: 'No'
analysis.box_integral.partition.additive: 'No'
analysis.box_integral.partition.basic: 'No'
analysis.box_integral.partition.filter: 'No'
analysis.box_integral.partition.measure: 'No'
analysis.box_integral.partition.split: 'No'
analysis.box_integral.partition.subbox_induction: 'No'
analysis.box_integral.partition.tagged: 'No'
analysis.calculus.affine_map: 'No'
analysis.calculus.bump_function_findim: 'No'
analysis.calculus.bump_function_inner: 'No'
analysis.calculus.conformal.inner_product: 'No'
analysis.calculus.conformal.normed_space: 'No'
analysis.calculus.cont_diff: 'No'
analysis.calculus.cont_diff_def: 'No'
analysis.calculus.darboux: 'No'
analysis.calculus.deriv: 'No'
analysis.calculus.diff_cont_on_cl: 'No'
analysis.calculus.dslope: 'No'
analysis.calculus.extend_deriv: 'No'
analysis.calculus.fderiv: 'No'
analysis.calculus.fderiv_analytic: 'No'
analysis.calculus.fderiv_measurable: 'No'
analysis.calculus.fderiv_symmetric: 'No'
analysis.calculus.formal_multilinear_series: 'No'
analysis.calculus.implicit: 'No'
analysis.calculus.inverse: 'No'
analysis.calculus.iterated_deriv: 'No'
analysis.calculus.lagrange_multipliers: 'No'
analysis.calculus.lhopital: 'No'
analysis.calculus.local_extr: 'No'
analysis.calculus.mean_value: 'No'
analysis.calculus.monotone: 'No'
analysis.calculus.parametric_integral: 'No'
analysis.calculus.parametric_interval_integral: 'No'
analysis.calculus.series: 'No'
analysis.calculus.tangent_cone: 'No'
analysis.calculus.taylor: 'No'
analysis.calculus.uniform_limits_deriv: 'No'
analysis.complex.abs_max: 'No'
analysis.complex.arg: 'No'
analysis.complex.basic: 'No'
analysis.complex.cauchy_integral: 'No'
analysis.complex.circle: 'No'
analysis.complex.conformal: 'No'
analysis.complex.isometry: 'No'
analysis.complex.liouville: 'No'
analysis.complex.locally_uniform_limit: 'No'
analysis.complex.open_mapping: 'No'
analysis.complex.operator_norm: 'No'
analysis.complex.phragmen_lindelof: 'No'
analysis.complex.polynomial: 'No'
analysis.complex.re_im_topology: 'No'
analysis.complex.real_deriv: 'No'
analysis.complex.removable_singularity: 'No'
analysis.complex.roots_of_unity: 'No'
analysis.complex.schwarz: 'No'
analysis.complex.unit_disc.basic: 'No'
analysis.complex.upper_half_plane.basic: 'No'
analysis.complex.upper_half_plane.functions_bounded_at_infty: 'No'
analysis.complex.upper_half_plane.metric: 'No'
analysis.complex.upper_half_plane.topology: 'No'
analysis.constant_speed: 'No'
analysis.convex.basic: 'No'
analysis.convex.between: 'No'
analysis.convex.body: 'No'
analysis.convex.caratheodory: 'No'
analysis.convex.combination: 'No'
analysis.convex.complex: 'No'
analysis.convex.cone.basic: 'No'
analysis.convex.contractible: 'No'
analysis.convex.exposed: 'No'
analysis.convex.extrema: 'No'
analysis.convex.extreme: 'No'
analysis.convex.function: 'No'
analysis.convex.gauge: 'No'
analysis.convex.hull: 'No'
analysis.convex.independent: 'No'
analysis.convex.integral: 'No'
analysis.convex.intrinsic: 'No'
analysis.convex.jensen: 'No'
analysis.convex.join: 'No'
analysis.convex.krein_milman: 'No'
analysis.convex.measure: 'No'
analysis.convex.normed: 'No'
analysis.convex.partition_of_unity: 'No'
analysis.convex.quasiconvex: 'No'
analysis.convex.segment: No mathlib4#3050 c5773405394e073885e2a144c9ca14637e8eb963
analysis.convex.side: 'No'
analysis.convex.simplicial_complex.basic: 'No'
analysis.convex.slope: 'No'
analysis.convex.specific_functions: 'No'
analysis.convex.star: No mathlib4#3050 9003f28797c0664a49e4179487267c494477d853
analysis.convex.stone_separation: 'No'
analysis.convex.strict: 'No'
analysis.convex.strict_convex_between: 'No'
analysis.convex.strict_convex_space: 'No'
analysis.convex.topology: 'No'
analysis.convex.uniform: 'No'
analysis.convolution: 'No'
analysis.fourier.add_circle: 'No'
analysis.fourier.fourier_transform: 'No'
analysis.fourier.poisson_summation: 'No'
analysis.fourier.riemann_lebesgue_lemma: 'No'
analysis.hofer: 'No'
analysis.inner_product_space.adjoint: 'No'
analysis.inner_product_space.basic: 'No'
analysis.inner_product_space.calculus: 'No'
analysis.inner_product_space.conformal_linear_map: 'No'
analysis.inner_product_space.dual: 'No'
analysis.inner_product_space.euclidean_dist: 'No'
analysis.inner_product_space.gram_schmidt_ortho: 'No'
analysis.inner_product_space.l2_space: 'No'
analysis.inner_product_space.lax_milgram: 'No'
analysis.inner_product_space.orientation: 'No'
analysis.inner_product_space.pi_L2: 'No'
analysis.inner_product_space.positive: 'No'
analysis.inner_product_space.projection: 'No'
analysis.inner_product_space.rayleigh: 'No'
analysis.inner_product_space.spectrum: 'No'
analysis.inner_product_space.symmetric: 'No'
analysis.inner_product_space.two_dim: 'No'
analysis.locally_convex.abs_convex: 'No'
analysis.locally_convex.balanced_core_hull: 'No'
analysis.locally_convex.basic: 'No'
analysis.locally_convex.bounded: 'No'
analysis.locally_convex.continuous_of_bounded: 'No'
analysis.locally_convex.polar: 'No'
analysis.locally_convex.weak_dual: 'No'
analysis.locally_convex.with_seminorms: 'No'
analysis.matrix: 'No'
analysis.mean_inequalities: 'No'
analysis.mean_inequalities_pow: 'No'
analysis.normed.field.basic: Yes mathlib4#2792 f06058e64b7e8397234455038f3f8aec83aaba5a
analysis.normed.field.infinite_sum: Yes mathlib4#2860 008205aa645b3f194c1da47025c5f110c8406eab
analysis.normed.field.unit_ball: Yes mathlib4#2857 3339976e2bcae9f1c81e620836d1eb736e3c4700
analysis.normed.group.SemiNormedGroup: 'No'
analysis.normed.group.SemiNormedGroup.completion: 'No'
analysis.normed.group.SemiNormedGroup.kernels: 'No'
analysis.normed.group.add_circle: 'No'
analysis.normed.group.add_torsor: 'No'
analysis.normed.group.ball_sphere: Yes mathlib4#2771 3339976e2bcae9f1c81e620836d1eb736e3c4700
analysis.normed.group.basic: Yes mathlib4#2736 195fcd60ff2bfe392543bceb0ec2adcdb472db4c
analysis.normed.group.completion: Yes mathlib4#2770 17ef379e997badd73e5eabb4d38f11919ab3c4b3
analysis.normed.group.controlled_closure: 'No'
analysis.normed.group.hom: Yes mathlib4#2748 3c4225288b55380a90df078ebae0991080b12393
analysis.normed.group.hom_completion: Yes mathlib4#2818 17ef379e997badd73e5eabb4d38f11919ab3c4b3
analysis.normed.group.infinite_sum: Yes mathlib4#2753 9a59dcb7a2d06bf55da57b9030169219980660cd
analysis.normed.group.pointwise: 'No'
analysis.normed.group.quotient: 'No'
analysis.normed.group.seminorm: Yes mathlib4#2400 28aa996fc6fb4317f0083c4e6daf79878d81be33
analysis.normed.order.basic: 'No'
analysis.normed.order.lattice: Yes mathlib4#2851 17ef379e997badd73e5eabb4d38f11919ab3c4b3
analysis.normed.order.upper_lower: 'No'
analysis.normed.ring.seminorm: 'No'
analysis.normed_space.M_structure: Yes mathlib4#2915 17ef379e997badd73e5eabb4d38f11919ab3c4b3
analysis.normed_space.add_torsor: 'No'
analysis.normed_space.add_torsor_bases: 'No'
analysis.normed_space.affine_isometry: 'No'
analysis.normed_space.algebra: 'No'
analysis.normed_space.ball_action: 'No'
analysis.normed_space.banach: 'No'
analysis.normed_space.banach_steinhaus: 'No'
analysis.normed_space.basic: 'No'
analysis.normed_space.bounded_linear_maps: 'No'
analysis.normed_space.compact_operator: 'No'
analysis.normed_space.complemented: 'No'
analysis.normed_space.completion: 'No'
analysis.normed_space.conformal_linear_map: 'No'
analysis.normed_space.continuous_affine_map: 'No'
analysis.normed_space.continuous_linear_map: 'No'
analysis.normed_space.dual: 'No'
analysis.normed_space.dual_number: 'No'
analysis.normed_space.enorm: 'No'
analysis.normed_space.exponential: 'No'
analysis.normed_space.extend: 'No'
analysis.normed_space.extr: 'No'
analysis.normed_space.finite_dimension: 'No'
analysis.normed_space.hahn_banach.extension: 'No'
analysis.normed_space.hahn_banach.separation: 'No'
analysis.normed_space.indicator_function: Yes mathlib4#2774 17ef379e997badd73e5eabb4d38f11919ab3c4b3
analysis.normed_space.int: Yes mathlib4#2848 5cc2dfdd3e92f340411acea4427d701dc7ed26f8
analysis.normed_space.is_R_or_C: 'No'
analysis.normed_space.linear_isometry: 'No'
analysis.normed_space.lp_equiv: 'No'
analysis.normed_space.lp_space: 'No'
analysis.normed_space.matrix_exponential: 'No'
analysis.normed_space.mazur_ulam: 'No'
analysis.normed_space.multilinear: 'No'
analysis.normed_space.operator_norm: 'No'
analysis.normed_space.pi_Lp: 'No'
analysis.normed_space.pointwise: 'No'
analysis.normed_space.quaternion_exponential: 'No'
analysis.normed_space.ray: 'No'
analysis.normed_space.riesz_lemma: 'No'
analysis.normed_space.spectrum: 'No'
analysis.normed_space.star.basic: 'No'
analysis.normed_space.star.continuous_functional_calculus: 'No'
analysis.normed_space.star.exponential: 'No'
analysis.normed_space.star.gelfand_duality: 'No'
analysis.normed_space.star.matrix: 'No'
analysis.normed_space.star.mul: 'No'
analysis.normed_space.star.multiplier: 'No'
analysis.normed_space.star.spectrum: 'No'
analysis.normed_space.triv_sq_zero_ext: 'No'
analysis.normed_space.units: 'No'
analysis.normed_space.weak_dual: 'No'
analysis.p_series: 'No'
analysis.quaternion: 'No'
analysis.schwartz_space: 'No'
analysis.seminorm: 'No'
analysis.special_functions.arsinh: 'No'
analysis.special_functions.bernstein: 'No'
analysis.special_functions.compare_exp: 'No'
analysis.special_functions.complex.arg: 'No'
analysis.special_functions.complex.circle: 'No'
analysis.special_functions.complex.log: 'No'
analysis.special_functions.complex.log_deriv: 'No'
analysis.special_functions.exp: 'No'
analysis.special_functions.exp_deriv: 'No'
analysis.special_functions.exponential: 'No'
analysis.special_functions.gamma: 'No'
analysis.special_functions.gaussian: 'No'
analysis.special_functions.integrals: 'No'
analysis.special_functions.japanese_bracket: 'No'
analysis.special_functions.log.base: 'No'
analysis.special_functions.log.basic: 'No'
analysis.special_functions.log.deriv: 'No'
analysis.special_functions.log.monotone: 'No'
analysis.special_functions.non_integrable: 'No'
analysis.special_functions.polar_coord: 'No'
analysis.special_functions.polynomials: 'No'
analysis.special_functions.pow: 'No'
analysis.special_functions.pow_deriv: 'No'
analysis.special_functions.sqrt: 'No'
analysis.special_functions.stirling: 'No'
analysis.special_functions.trigonometric.angle: 'No'
analysis.special_functions.trigonometric.arctan: 'No'
analysis.special_functions.trigonometric.arctan_deriv: 'No'
analysis.special_functions.trigonometric.basic: 'No'
analysis.special_functions.trigonometric.bounds: 'No'
analysis.special_functions.trigonometric.chebyshev: 'No'
analysis.special_functions.trigonometric.complex: 'No'
analysis.special_functions.trigonometric.complex_deriv: 'No'
analysis.special_functions.trigonometric.deriv: 'No'
analysis.special_functions.trigonometric.euler_sine_prod: 'No'
analysis.special_functions.trigonometric.inverse: 'No'
analysis.special_functions.trigonometric.inverse_deriv: 'No'
analysis.special_functions.trigonometric.series: 'No'
analysis.specific_limits.basic: 'No'
analysis.specific_limits.floor_pow: 'No'
analysis.specific_limits.normed: 'No'
analysis.subadditive: Yes mathlib4#2772 f2ce6086713c78a7f880485f7917ea547a215982
analysis.sum_integral_comparisons: 'No'
analysis.von_neumann_algebra.basic: 'No'
category_theory.Fintype: 'No'
category_theory.abelian.basic: No mathlib4#2769 8c75ef3517d4106e89fe524e6281d0b0545f47fc
category_theory.abelian.diagram_lemmas.four: 'No'
category_theory.abelian.exact: 'No'
category_theory.abelian.ext: 'No'
category_theory.abelian.functor_category: 'No'
category_theory.abelian.generator: 'No'
category_theory.abelian.homology: 'No'
category_theory.abelian.images: Yes mathlib4#2676 9e7c80f638149bfb3504ba8ff48dfdbfc949fb1a
category_theory.abelian.injective: 'No'
category_theory.abelian.injective_resolution: 'No'
category_theory.abelian.left_derived: 'No'
category_theory.abelian.non_preadditive: Yes mathlib4#2752 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
category_theory.abelian.opposite: 'No'
category_theory.abelian.projective: 'No'
category_theory.abelian.pseudoelements: 'No'
category_theory.abelian.right_derived: 'No'
category_theory.abelian.subobject: 'No'
category_theory.abelian.transfer: 'No'
category_theory.action: 'No'
category_theory.additive.basic: No mathlib4#2797 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
category_theory.adhesive: 'No'
category_theory.adjunction.adjoint_functor_theorems: 'No'
category_theory.adjunction.basic: Yes mathlib4#2198 d101e93197bb5f6ea89bd7ba386b7f7dff1f3903
category_theory.adjunction.comma: Yes mathlib4#2591 8a318021995877a44630c898d0b2bc376fceef3b
category_theory.adjunction.evaluation: Yes mathlib4#2698 937c692d73f5130c7fecd3fd32e81419f4e04eb7
category_theory.adjunction.fully_faithful: Yes mathlib4#2418 9e7c80f638149bfb3504ba8ff48dfdbfc949fb1a
category_theory.adjunction.lifting: 'No'
category_theory.adjunction.limits: Yes mathlib4#2683 9e7c80f638149bfb3504ba8ff48dfdbfc949fb1a
category_theory.adjunction.mates: Yes mathlib4#2455 cea27692b3fdeb328a2ddba6aabf181754543184
category_theory.adjunction.opposites: No mathlib4#2424 f3ee4628e2dc737653af924c41fa681abc2a4f4a
category_theory.adjunction.over: 'No'
category_theory.adjunction.reflective: Yes mathlib4#2467 239d882c4fb58361ee8b3b39fb2091320edef10a
category_theory.adjunction.whiskering: Yes mathlib4#2408 28aa996fc6fb4317f0083c4e6daf79878d81be33
category_theory.arrow: Yes mathlib4#2315 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.balanced: Yes mathlib4#2313 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.bicategory.End: Yes mathlib4#2454 6abb6de90754c5613a3aab6261eea9e5c72d539d
category_theory.bicategory.basic: Yes mathlib4#2126 4c19a16e4b705bf135cf9a80ac18fcc99c438514
category_theory.bicategory.coherence: 'No'
category_theory.bicategory.coherence_tactic: 'No'
category_theory.bicategory.free: No mathlib4#2482 3d7987cda72abc473c7cdbbb075170e9ac620042
category_theory.bicategory.functor: Yes mathlib4#2301 369525b73f229ccd76a6ec0e0e0bf2be57599768
category_theory.bicategory.functor_bicategory: 'No'
category_theory.bicategory.locally_discrete: Yes mathlib4#2813 c9c9fa15fec7ca18e9ec97306fb8764bfe988a7e
category_theory.bicategory.natural_transformation: 'No'
category_theory.bicategory.single_obj: 'No'
category_theory.bicategory.strict: Yes mathlib4#2218 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.category.Bipointed: Yes mathlib4#2931 c8ab806ef73c20cab1d87b5157e43a82c205f28e
category_theory.category.Cat: Yes mathlib4#2375 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
category_theory.category.Cat.limit: Yes mathlib4#2834 1995c7bbdbb0adb1b6d5acdc654f6cf46ed96cfa
category_theory.category.Groupoid: 'No'
category_theory.category.Kleisli: Yes mathlib4#843 70d50ecfd4900dd6d328da39ab7ebd516abe4025
category_theory.category.PartialFun: 'No'
category_theory.category.Pointed: Yes mathlib4#2864 c8ab806ef73c20cab1d87b5157e43a82c205f28e
category_theory.category.Quiv: Yes mathlib4#2865 350a381705199e9a070f84e98e803c3c25a97a4c
category_theory.category.Rel: Yes mathlib4#822 afad8e438d03f9d89da2914aa06cb4964ba87a18
category_theory.category.Twop: 'No'
category_theory.category.basic: Yes mathlib4#749 8350c34a64b9bc3fc64335df8006bffcadc7baa6
category_theory.category.galois_connection: Yes mathlib4#2440 d82b87871d9a274884dff5263fa4f5d93bcce1d6
category_theory.category.pairwise: Yes mathlib4#2534 d82b87871d9a274884dff5263fa4f5d93bcce1d6
category_theory.category.preorder: Yes mathlib4#2206 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.category.ulift: Yes mathlib4#2312 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.closed.cartesian: 'No'
category_theory.closed.functor: 'No'
category_theory.closed.functor_category: 'No'
category_theory.closed.ideal: 'No'
category_theory.closed.monoidal: Yes mathlib4#3002 c0e00a871b9f6d3aca7c10fb3abdc8720a2c5313
category_theory.closed.types: 'No'
category_theory.closed.zero: 'No'
category_theory.cofiltered_system: 'No'
category_theory.comm_sq: Yes mathlib4#2322 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.comma: Yes mathlib4#2260 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.concrete_category.basic: Yes mathlib4#2619 05b820ec79b3c98a7dbf1cb32e181584166da2ca
category_theory.concrete_category.bundled: Yes mathlib4#514 a148d797a1094ab554ad4183a4ad6f130358ef64
category_theory.concrete_category.bundled_hom: Yes mathlib4#2740 77ca1ed347337ecbafa9d9f4a55e330e44e9f9f8
category_theory.concrete_category.elementwise: No mathlib4#2901 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.concrete_category.reflects_isomorphisms: Yes mathlib4#2739 73dd4b5411ec8fafb18a9d77c9c826907730af80
category_theory.concrete_category.unbundled_hom: 'No'
category_theory.conj: Yes mathlib4#2316 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.connected_components: Yes mathlib4#2843 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.core: Yes mathlib4#2305 369525b73f229ccd76a6ec0e0e0bf2be57599768
category_theory.differential_object: 'No'
category_theory.discrete_category: Yes mathlib4#2326 369525b73f229ccd76a6ec0e0e0bf2be57599768
category_theory.elements: No mathlib4#2815 8a318021995877a44630c898d0b2bc376fceef3b
category_theory.elementwise: Yes mathlib4#2872 70fd9563a21e7b963887c9360bd29b2393e6225a
  blocked by missing elementwise tactic
category_theory.endofunctor.algebra: 'No'
category_theory.endomorphism: Yes mathlib4#2310 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.enriched.basic: 'No'
category_theory.epi_mono: Yes mathlib4#2292 48085f140e684306f9e7da907cd5932056d1aded
category_theory.eq_to_hom: Yes mathlib4#2207 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.equivalence: Yes mathlib4#1287 9aba7801eeecebb61f58a5763c2b6dd1b47dc6ef
category_theory.essential_image: Yes mathlib4#1132 550b58538991c8977703fdeb7c9d51a5aa27df11
category_theory.essentially_small: Yes mathlib4#2452 f7707875544ef1f81b32cb68c79e0e24e45a0e76
category_theory.extensive: 'No'
category_theory.filtered: Yes mathlib4#2493 14e80e85cbca5872a329fbfd3d1f3fd64e306934
category_theory.fin_category: Yes mathlib4#2423 c3019c79074b0619edb4b27553a91b2e82242395
category_theory.full_subcategory: Yes mathlib4#1126 550b58538991c8977703fdeb7c9d51a5aa27df11
category_theory.functor.basic: Yes mathlib4#749 8350c34a64b9bc3fc64335df8006bffcadc7baa6
category_theory.functor.category: Yes mathlib4#749 8350c34a64b9bc3fc64335df8006bffcadc7baa6
category_theory.functor.const: Yes mathlib4#2208 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.functor.currying: Yes mathlib4#2298 369525b73f229ccd76a6ec0e0e0bf2be57599768
category_theory.functor.epi_mono: Yes mathlib4#2331 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.functor.flat: 'No'
category_theory.functor.fully_faithful: Yes mathlib4#846 70d50ecfd4900dd6d328da39ab7ebd516abe4025
category_theory.functor.functorial: Yes mathlib4#822 afad8e438d03f9d89da2914aa06cb4964ba87a18
category_theory.functor.hom: Yes mathlib4#2295 369525b73f229ccd76a6ec0e0e0bf2be57599768
category_theory.functor.inv_isos: Yes mathlib4#2237 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.functor.left_derived: 'No'
category_theory.functor.reflects_isomorphisms: Yes mathlib4#2332 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.generator: 'No'
category_theory.glue_data: 'No'
category_theory.graded_object: 'No'
category_theory.grothendieck: 'No'
category_theory.groupoid: Yes mathlib4#2282 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.groupoid.basic: Yes mathlib4#2335 740acc0e6f9adf4423f92a485d0456fc271482da
category_theory.groupoid.free_groupoid: 'No'
category_theory.groupoid.subgroupoid: 'No'
category_theory.groupoid.vertex_group: Yes mathlib4#2609 47b51515e69f59bca5cf34ef456e6000fe205a69
category_theory.idempotents.basic: 'No'
category_theory.idempotents.biproducts: 'No'
category_theory.idempotents.functor_categories: 'No'
category_theory.idempotents.functor_extension: 'No'
category_theory.idempotents.homological_complex: 'No'
category_theory.idempotents.karoubi: 'No'
category_theory.idempotents.karoubi_karoubi: 'No'
category_theory.idempotents.simplicial_object: 'No'
category_theory.is_connected: Yes mathlib4#2443 024a4231815538ac739f52d08dd20a55da0d6b23
category_theory.isomorphism: Yes mathlib4#749 8350c34a64b9bc3fc64335df8006bffcadc7baa6
category_theory.isomorphism_classes: Yes mathlib4#2394 28aa996fc6fb4317f0083c4e6daf79878d81be33
category_theory.lifting_properties.adjunction: Yes mathlib4#2329 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.lifting_properties.basic: Yes mathlib4#2325 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.limits.bicones: Yes mathlib4#2775 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.limits.colimit_limit: Yes mathlib4#2810 59382264386afdbaf1727e617f5fdda511992eb9
category_theory.limits.comma: Yes mathlib4#2776 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.limits.concrete_category: No mathlib4#3023 c3019c79074b0619edb4b27553a91b2e82242395
category_theory.limits.cone_category: Yes mathlib4#2767 18302a460eb6a071cf0bfe11a4df025c8f8af244
category_theory.limits.cones: Yes mathlib4#2337 740acc0e6f9adf4423f92a485d0456fc271482da
category_theory.limits.connected: Yes mathlib4#2830 d6814c584384ddf2825ff038e868451a7c956f31
category_theory.limits.constructions.binary_products: Yes mathlib4#2699 3424a5932a77dcec2c177ce7d805acace6149299
category_theory.limits.constructions.epi_mono: Yes mathlib4#2573 f7baecbb54bd0f24f228576f97b1752fc3c9b318
category_theory.limits.constructions.equalizers: Yes mathlib4#2700 3424a5932a77dcec2c177ce7d805acace6149299
category_theory.limits.constructions.filtered: Yes mathlib4#2832 e4ee4e30418efcb8cf304ba76ad653aeec04ba6e
category_theory.limits.constructions.finite_products_of_binary_products: Yes mathlib4#2738
  ac3ae212f394f508df43e37aa093722fa9b65d31
category_theory.limits.constructions.limits_of_products_and_equalizers: Yes mathlib4#2764
  c3019c79074b0619edb4b27553a91b2e82242395
category_theory.limits.constructions.over.connected: Yes mathlib4#2831 d6814c584384ddf2825ff038e868451a7c956f31
category_theory.limits.constructions.over.default: No do not port default files
category_theory.limits.constructions.over.products: 'No'
category_theory.limits.constructions.pullbacks: Yes mathlib4#2658 cd7a8a184d7c5635e30083eabc4baf5589c30b7a
category_theory.limits.constructions.weakly_initial: 'No'
category_theory.limits.constructions.zero_objects: Yes mathlib4#2823 52a270e2ea4e342c2587c106f8be904524214a4b
category_theory.limits.creates: Yes mathlib4#2646 fe5e4ce6c72d96d77ad40ac832a6e7f8040990bc
category_theory.limits.essentially_small: Yes mathlib4#2778 952e7ee9eaf835f322f2d01ca6cf06ed0ab6d2c5
category_theory.limits.exact_functor: Yes mathlib4#2697 9fc53308a90fac244ac715308e1f9c969e6843a4
category_theory.limits.filtered: Yes mathlib4#2541 e4ee4e30418efcb8cf304ba76ad653aeec04ba6e
category_theory.limits.filtered_colimit_commutes_finite_limit: 'No'
category_theory.limits.final: Yes mathlib4#2820 8a318021995877a44630c898d0b2bc376fceef3b
category_theory.limits.fubini: 'No'
category_theory.limits.full_subcategory: Yes mathlib4#2690 fe5e4ce6c72d96d77ad40ac832a6e7f8040990bc
category_theory.limits.functor_category: Yes mathlib4#2380 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
category_theory.limits.has_limits: Yes mathlib4#2368 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
category_theory.limits.is_limit: Yes mathlib4#2354 740acc0e6f9adf4423f92a485d0456fc271482da
category_theory.limits.kan_extension: Yes mathlib4#2601 c9c9fa15fec7ca18e9ec97306fb8764bfe988a7e
category_theory.limits.lattice: Yes mathlib4#2787 c3019c79074b0619edb4b27553a91b2e82242395
category_theory.limits.mono_coprod: Yes mathlib4#2803 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.limits.opposites: Yes mathlib4#2805 ac3ae212f394f508df43e37aa093722fa9b65d31
category_theory.limits.over: 'No'
category_theory.limits.pi: Yes mathlib4#2854 744d59af0b28d0c42f631038627df9b85ae1d1ce
category_theory.limits.preserves.basic: Yes mathlib4#2377 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
category_theory.limits.preserves.filtered: Yes mathlib4#2749 c43486ecf2a5a17479a32ce09e4818924145e90e
category_theory.limits.preserves.finite: Yes mathlib4#2648 024a4231815538ac739f52d08dd20a55da0d6b23
category_theory.limits.preserves.functor_category: 'No'
category_theory.limits.preserves.limits: Yes mathlib4#2379 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
category_theory.limits.preserves.opposites: Yes mathlib4#2826 9ed4366659f4fcca0ee70310d26ac5518dcb6dd0
category_theory.limits.preserves.shapes.binary_products: Yes mathlib4#2654 024a4231815538ac739f52d08dd20a55da0d6b23
category_theory.limits.preserves.shapes.biproducts: Yes mathlib4#2727 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.limits.preserves.shapes.equalizers: Yes mathlib4#2687 4698e35ca56a0d4fa53aa5639c3364e0a77f4eba
category_theory.limits.preserves.shapes.images: Yes mathlib4#2824 fc78e3c190c72a109699385da6be2725e88df841
category_theory.limits.preserves.shapes.kernels: Yes mathlib4#2806 956af7c76589f444f2e1313911bad16366ea476d
category_theory.limits.preserves.shapes.products: Yes mathlib4#2656 024a4231815538ac739f52d08dd20a55da0d6b23
category_theory.limits.preserves.shapes.pullbacks: Yes mathlib4#2571 f11e306adb9f2a393539d2bb4293bf1b42caa7ac
category_theory.limits.preserves.shapes.terminal: Yes mathlib4#2579 bbe25d4d92565a5fd773e52e041a90387eee3c93
category_theory.limits.preserves.shapes.zero: Yes mathlib4#2622 bbe25d4d92565a5fd773e52e041a90387eee3c93
category_theory.limits.presheaf: 'No'
category_theory.limits.shapes.binary_products: Yes mathlib4#2507 fec1d95fc61c750c1ddbb5b1f7f48b8e811a80d7
category_theory.limits.shapes.biproducts: Yes mathlib4#2710 ac3ae212f394f508df43e37aa093722fa9b65d31
category_theory.limits.shapes.comm_sq: Yes mathlib4#2867 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.limits.shapes.concrete_category: 'No'
category_theory.limits.shapes.diagonal: No mathlib4#2949 f6bab67886fb92c3e2f539cc90a83815f69a189d
category_theory.limits.shapes.disjoint_coproduct: Yes mathlib4#2689 c9c9fa15fec7ca18e9ec97306fb8764bfe988a7e
category_theory.limits.shapes.equalizers: Yes mathlib4#2562 4698e35ca56a0d4fa53aa5639c3364e0a77f4eba
category_theory.limits.shapes.equivalence: Yes mathlib4#2694 ea74dc9f981009c33b9971f3389509a88c95cf07
category_theory.limits.shapes.finite_limits: Yes mathlib4#2647 c3019c79074b0619edb4b27553a91b2e82242395
category_theory.limits.shapes.finite_products: Yes mathlib4#2688 ac3ae212f394f508df43e37aa093722fa9b65d31
category_theory.limits.shapes.functor_category: Yes mathlib4#2716 024a4231815538ac739f52d08dd20a55da0d6b23
category_theory.limits.shapes.images: Yes mathlib4#2615 563aed347eb59dc4181cb732cda0d124d736eaa3
category_theory.limits.shapes.kernel_pair: Yes mathlib4#2871 f6bab67886fb92c3e2f539cc90a83815f69a189d
category_theory.limits.shapes.kernels: Yes mathlib4#2636 956af7c76589f444f2e1313911bad16366ea476d
category_theory.limits.shapes.multiequalizer: Yes mathlib4#2786 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.limits.shapes.normal_mono.basic: Yes mathlib4#2732 bbe25d4d92565a5fd773e52e041a90387eee3c93
category_theory.limits.shapes.normal_mono.equalizers: Yes mathlib4#2737 3a061790136d13594ec10c7c90d202335ac5d854
category_theory.limits.shapes.products: Yes mathlib4#2564 e11bafa5284544728bd3b189942e930e0d4701de
category_theory.limits.shapes.pullbacks: Yes mathlib4#2522 7316286ff2942aa14e540add9058c6b0aa1c8070
category_theory.limits.shapes.reflexive: Yes mathlib4#3041 d6814c584384ddf2825ff038e868451a7c956f31
category_theory.limits.shapes.regular_mono: Yes mathlib4#2686 239d882c4fb58361ee8b3b39fb2091320edef10a
category_theory.limits.shapes.split_coequalizer: Yes mathlib4#2655 024a4231815538ac739f52d08dd20a55da0d6b23
category_theory.limits.shapes.strict_initial: Yes mathlib4#2695 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.limits.shapes.strong_epi: Yes mathlib4#2327 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.limits.shapes.terminal: Yes mathlib4#2459 239d882c4fb58361ee8b3b39fb2091320edef10a
category_theory.limits.shapes.types: No mathlib4#2809 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.limits.shapes.wide_equalizers: No mathlib4#2713 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.limits.shapes.wide_pullbacks: Yes mathlib4#2453 f187f1074fa1857c94589cc653c786cadc4c35ff
category_theory.limits.shapes.zero_morphisms: Yes mathlib4#2621 f7707875544ef1f81b32cb68c79e0e24e45a0e76
category_theory.limits.shapes.zero_objects: Yes mathlib4#2594 74333bd53d25b6809203a2bfae80eea5fc1fc076
category_theory.limits.small_complete: Yes mathlib4#2731 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.limits.types: Yes mathlib4#2712 4aa2a2e17940311e47007f087c9df229e7f12942
category_theory.limits.unit: Yes mathlib4#2597 c85d2ff93210de84373ab4c9c6dba2b78494961e
category_theory.limits.yoneda: Yes mathlib4#2381 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
category_theory.linear.basic: Yes mathlib4#2744 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
category_theory.linear.functor_category: Yes mathlib4#2793 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
category_theory.linear.linear_functor: Yes mathlib4#2814 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
category_theory.linear.yoneda: 'No'
category_theory.localization.construction: No mathlib4#2949 1a5e56f2166e4e9d0964c71f4273b1d39227678d
category_theory.localization.opposite: No mathlib4#2949 8efef279998820353694feb6ff5631ed0d309ecc
category_theory.localization.predicate: No mathlib4#2949 8efef279998820353694feb6ff5631ed0d309ecc
category_theory.monad.adjunction: 'No'
category_theory.monad.algebra: 'No'
category_theory.monad.basic: No mathlib4#2969 1995c7bbdbb0adb1b6d5acdc654f6cf46ed96cfa
category_theory.monad.coequalizer: 'No'
category_theory.monad.equiv_mon: 'No'
category_theory.monad.kleisli: 'No'
category_theory.monad.limits: 'No'
category_theory.monad.monadicity: 'No'
category_theory.monad.products: 'No'
category_theory.monad.types: 'No'
category_theory.monoidal.Bimod: 'No'
category_theory.monoidal.CommMon_: 'No'
category_theory.monoidal.End: Yes mathlib4#2759 85075bccb68ab7fa49fb05db816233fb790e4fe9
category_theory.monoidal.Mod: 'No'
category_theory.monoidal.Mon_: 'No'
category_theory.monoidal.braided: 'No'
category_theory.monoidal.category: Yes mathlib4#2318 32253a1a1071173b33dc7d6a218cf722c6feb514
category_theory.monoidal.center: 'No'
category_theory.monoidal.coherence: 'No'
category_theory.monoidal.coherence_lemmas: 'No'
category_theory.monoidal.discrete: No mathlib4#3047 8a0e71287eb4c80e87f72e8c174835f360a6ddd9
category_theory.monoidal.free.basic: No mathlib4#2808 14b69e9f3c16630440a2cbd46f1ddad0d561dee7
category_theory.monoidal.free.coherence: 'No'
category_theory.monoidal.functor: Yes mathlib4#2445 3d7987cda72abc473c7cdbbb075170e9ac620042
category_theory.monoidal.functor_category: 'No'
category_theory.monoidal.functorial: Yes mathlib4#2504 73dd4b5411ec8fafb18a9d77c9c826907730af80
category_theory.monoidal.internal.Module: 'No'
category_theory.monoidal.internal.functor_category: 'No'
category_theory.monoidal.internal.limits: 'No'
category_theory.monoidal.internal.types: 'No'
category_theory.monoidal.limits: 'No'
category_theory.monoidal.linear: 'No'
category_theory.monoidal.natural_transformation: No mathlib4#3047 d047eb4671130d5998b185e49a0443a0d2e9b191
category_theory.monoidal.of_chosen_finite_products: 'No'
category_theory.monoidal.of_has_finite_products: 'No'
category_theory.monoidal.opposite: 'No'
category_theory.monoidal.preadditive: Yes mathlib4#3033 986c4d5761f938b2e1c43c01f001b6d9d88c2055
category_theory.monoidal.rigid.basic: 'No'
category_theory.monoidal.rigid.functor_category: 'No'
category_theory.monoidal.rigid.of_equivalence: 'No'
category_theory.monoidal.skeleton: 'No'
category_theory.monoidal.subcategory: 'No'
category_theory.monoidal.tor: 'No'
category_theory.monoidal.transport: 'No'
category_theory.monoidal.types: 'No'
category_theory.morphism_property: No mathlib4#2949 7f963633766aaa3ebc8253100a5229dd463040c7
category_theory.natural_isomorphism: Yes mathlib4#820 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904
category_theory.natural_transformation: Yes mathlib4#749 8350c34a64b9bc3fc64335df8006bffcadc7baa6
category_theory.noetherian: 'No'
category_theory.opposites: Yes mathlib4#2195 dde670c9a3f503647fd5bfdf1037bad526d3397a
category_theory.over: Yes mathlib4#2496 8a318021995877a44630c898d0b2bc376fceef3b
category_theory.path_category: Yes mathlib4#2580 c6dd521ebdce53bb372c527569dd7c25de53a08b
category_theory.pempty: Yes mathlib4#2363 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
category_theory.pi.basic: Yes mathlib4#2230 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.preadditive.Mat: 'No'
category_theory.preadditive.additive_functor: Yes mathlib4#2779 ee89acdf96a0b45afe3eea493bceb2a80a0f2efa
category_theory.preadditive.basic: Yes mathlib4#2735 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
category_theory.preadditive.biproducts: Yes mathlib4#2760 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
category_theory.preadditive.eilenberg_moore: 'No'
category_theory.preadditive.endo_functor: 'No'
category_theory.preadditive.functor_category: Yes mathlib4#2746 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
category_theory.preadditive.generator: 'No'
category_theory.preadditive.hom_orthogonal: 'No'
category_theory.preadditive.injective: 'No'
category_theory.preadditive.injective_resolution: 'No'
category_theory.preadditive.left_exact: Yes mathlib4#2853 70fd9563a21e7b963887c9360bd29b2393e6225a
category_theory.preadditive.of_biproducts: Yes mathlib4#2939 061ea99a5610cfc72c286aa930d3c1f47f74f3d0
category_theory.preadditive.opposite: 'No'
category_theory.preadditive.projective: 'No'
category_theory.preadditive.projective_resolution: 'No'
category_theory.preadditive.schur: 'No'
category_theory.preadditive.single_obj: Yes mathlib4#3030 829895f162a1f29d0133f4b3538f4cd1fb5bffd3
category_theory.preadditive.yoneda.basic: 'No'
category_theory.preadditive.yoneda.limits: 'No'
category_theory.products.associator: Yes mathlib4#2274 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.products.basic: Yes mathlib4#2211 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.products.bifunctor: Yes mathlib4#2239 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.punit: Yes mathlib4#2367 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
category_theory.quotient: Yes mathlib4#2339 740acc0e6f9adf4423f92a485d0456fc271482da
category_theory.shift: No mathlib4#3047 14b69e9f3c16630440a2cbd46f1ddad0d561dee7
category_theory.sigma.basic: Yes mathlib4#1147 ba2245edf0c8bb155f1569fd9b9492a9b384cde6
category_theory.simple: 'No'
category_theory.single_obj: Yes mathlib4#3021 56adee5b5eef9e734d82272918300fca4f3e7cef
category_theory.sites.adjunction: 'No'
category_theory.sites.canonical: 'No'
category_theory.sites.closed: 'No'
category_theory.sites.compatible_plus: 'No'
category_theory.sites.compatible_sheafification: 'No'
category_theory.sites.cover_lifting: 'No'
category_theory.sites.cover_preserving: 'No'
category_theory.sites.dense_subsite: 'No'
category_theory.sites.grothendieck: No mathlib4#2795 14b69e9f3c16630440a2cbd46f1ddad0d561dee7
category_theory.sites.induced_topology: 'No'
category_theory.sites.left_exact: 'No'
category_theory.sites.limits: 'No'
category_theory.sites.plus: 'No'
category_theory.sites.pretopology: 'No'
category_theory.sites.pushforward: 'No'
category_theory.sites.sheaf: 'No'
category_theory.sites.sheaf_of_types: 'No'
category_theory.sites.sheafification: 'No'
category_theory.sites.sieves: Yes mathlib4#2691 239d882c4fb58361ee8b3b39fb2091320edef10a
category_theory.sites.spaces: 'No'
category_theory.sites.subsheaf: 'No'
category_theory.sites.surjective: 'No'
category_theory.sites.types: 'No'
category_theory.sites.whiskering: 'No'
category_theory.skeletal: Yes mathlib4#2432 28aa996fc6fb4317f0083c4e6daf79878d81be33
category_theory.structured_arrow: Yes mathlib4#2486 fef8efdf78f223294c34a41875923ab1272322d4
category_theory.subobject.basic: 'No'
category_theory.subobject.comma: 'No'
category_theory.subobject.factor_thru: 'No'
category_theory.subobject.lattice: 'No'
category_theory.subobject.limits: 'No'
category_theory.subobject.mono_over: 'No'
category_theory.subobject.types: 'No'
category_theory.subobject.well_powered: 'No'
category_theory.subterminal: 'No'
category_theory.sums.associator: Yes mathlib4#2447 590f43db91071eb3134fef935ec9d7cd2a3bd4ce
category_theory.sums.basic: Yes mathlib4#2246 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
category_theory.thin: Yes mathlib4#822 afad8e438d03f9d89da2914aa06cb4964ba87a18
category_theory.triangulated.basic: No mathlib4#3047 f7707875544ef1f81b32cb68c79e0e24e45a0e76
category_theory.triangulated.pretriangulated: 'No'
category_theory.triangulated.rotate: No mathlib4#3047 19786714ebe478f40b503acb4705fb058ba47303
category_theory.triangulated.triangulated: 'No'
category_theory.types: Yes mathlib4#2294 48085f140e684306f9e7da907cd5932056d1aded
category_theory.whiskering: Yes mathlib4#1071 d012cd09a9b256d870751284dd6a29882b0be105
category_theory.with_terminal: No mathlib4#2630 14b69e9f3c16630440a2cbd46f1ddad0d561dee7
category_theory.yoneda: Yes mathlib4#2299 369525b73f229ccd76a6ec0e0e0bf2be57599768
combinatorics.additive.behrend: 'No'
combinatorics.additive.energy: Yes mathlib4#1702 509de852e1de55e1efa8eacfa11df0823f26f226
combinatorics.additive.pluennecke_ruzsa: Yes mathlib4#2433 4aab2abced69a9e579b1e6dc2856ed3db48e2cbd
combinatorics.additive.ruzsa_covering: Yes mathlib4#2065 b363547b3113d350d053abdf2884e9850a56b205
combinatorics.additive.salem_spencer: 'No'
combinatorics.catalan: Yes mathlib4#2588 26b40791e4a5772a4e53d0e28e4df092119dc7da
combinatorics.colex: Yes mathlib4#1926 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
combinatorics.composition: Yes mathlib4#2043 2705404e701abc6b3127da906f40bae062a169c9
combinatorics.configuration: 'No'
combinatorics.derangements.basic: Yes mathlib4#2530 9407b03373c8cd201df99d6bc5514fc2db44054f
combinatorics.derangements.exponential: 'No'
combinatorics.derangements.finite: 'No'
combinatorics.double_counting: Yes mathlib4#1715 1126441d6bccf98c81214a0780c73d499f6721fe
combinatorics.hales_jewett: Yes mathlib4#1704 1126441d6bccf98c81214a0780c73d499f6721fe
combinatorics.hall.basic: 'No'
combinatorics.hall.finite: Yes mathlib4#1763 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
combinatorics.hindman: Yes mathlib4#2280 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
combinatorics.partition: Yes mathlib4#2264 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
combinatorics.pigeonhole: Yes mathlib4#1758 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
combinatorics.quiver.arborescence: Yes mathlib4#997 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
combinatorics.quiver.basic: Yes mathlib4#749 56adee5b5eef9e734d82272918300fca4f3e7cef
combinatorics.quiver.cast: Yes mathlib4#990 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
combinatorics.quiver.connected_component: Yes mathlib4#836 18a5306c091183ac90884daa9373fa3b178e8607
combinatorics.quiver.path: Yes mathlib4#811 18a5306c091183ac90884daa9373fa3b178e8607
combinatorics.quiver.push: Yes mathlib4#868 2258b40dacd2942571c8ce136215350c702dc78f
combinatorics.quiver.single_obj: Yes mathlib4#1686 509de852e1de55e1efa8eacfa11df0823f26f226
combinatorics.quiver.subquiver: Yes mathlib4#828 70d50ecfd4900dd6d328da39ab7ebd516abe4025
combinatorics.quiver.symmetric: Yes mathlib4#971 706d88f2b8fdfeb0b22796433d7a6c1a010af9f2
combinatorics.set_family.compression.down: Yes mathlib4#1604 9003f28797c0664a49e4179487267c494477d853
combinatorics.set_family.compression.uv: Yes mathlib4#1600 9003f28797c0664a49e4179487267c494477d853
combinatorics.set_family.harris_kleitman: Yes mathlib4#2060 b363547b3113d350d053abdf2884e9850a56b205
combinatorics.set_family.intersecting: Yes mathlib4#2005 d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
combinatorics.set_family.kleitman: Yes mathlib4#2071 4c19a16e4b705bf135cf9a80ac18fcc99c438514
combinatorics.set_family.lym: Yes mathlib4#1969 861a26926586cd46ff80264d121cdb6fa0e35cc1
combinatorics.set_family.shadow: Yes mathlib4#1938 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
combinatorics.simple_graph.acyclic: Yes mathlib4#2559 b07688016d62f81d14508ff339ea3415558d6353
combinatorics.simple_graph.adj_matrix: 'No'
combinatorics.simple_graph.basic: Yes mathlib4#1883 db53863fb135228820ee0b08e8dce9349a3d911b
combinatorics.simple_graph.clique: Yes mathlib4#2489 cd7f0626a0b04be1dda223a26123313514a55fb4
combinatorics.simple_graph.coloring: Yes mathlib4#2526 70fd9563a21e7b963887c9360bd29b2393e6225a
combinatorics.simple_graph.connectivity: Yes mathlib4#2514 13cd3e89b30352d5b1b7349f5537ea18ba878e40
combinatorics.simple_graph.degree_sum: Yes mathlib4#2895 90659cbe25e59ec302e2fb92b00e9732160cc620
combinatorics.simple_graph.density: Yes mathlib4#2492 a4ec43f53b0bd44c697bcc3f5a62edd56f269ef1
combinatorics.simple_graph.ends.defs: 'No'
combinatorics.simple_graph.ends.properties: 'No'
combinatorics.simple_graph.finsubgraph: 'No'
combinatorics.simple_graph.hasse: Yes mathlib4#2582 8a38a697305292b37a61650e2c3bd3502d98c805
combinatorics.simple_graph.inc_matrix: 'No'
combinatorics.simple_graph.matching: 'No'
combinatorics.simple_graph.metric: Yes mathlib4#2572 352ecfe114946c903338006dd3287cb5a9955ff2
combinatorics.simple_graph.partition: Yes mathlib4#2536 2303b3e299f1c75b07bceaaac130ce23044d1386
combinatorics.simple_graph.prod: Yes mathlib4#2565 2985fa3c31a27274aed06c433510bc14b73d6488
combinatorics.simple_graph.regularity.bound: 'No'
combinatorics.simple_graph.regularity.energy: Yes mathlib4#2575 f7707875544ef1f81b32cb68c79e0e24e45a0e76
combinatorics.simple_graph.regularity.equitabilise: Yes mathlib4#2087 4c19a16e4b705bf135cf9a80ac18fcc99c438514
combinatorics.simple_graph.regularity.uniform: Yes mathlib4#2547 32b08ef840dd25ca2e47e035c5da03ce16d2dc3c
combinatorics.simple_graph.strongly_regular: Yes mathlib4#2476 2b35fc7bea4640cb75e477e83f32fbd538920822
combinatorics.simple_graph.subgraph: Yes mathlib4#2495 d6e84a0d3db8910c99b3aa0c56be88fa8bab6f80
combinatorics.simple_graph.trails: Yes mathlib4#2574 edaaaa4a5774e6623e0ddd919b2f2db49c65add4
combinatorics.simple_graph.triangle.basic: Yes mathlib4#2494 cd7f0626a0b04be1dda223a26123313514a55fb4
combinatorics.young.semistandard_tableau: Yes mathlib4#2067 b363547b3113d350d053abdf2884e9850a56b205
combinatorics.young.young_diagram: Yes mathlib4#1994 59694bd07f0a39c5beccba34bd9f413a160782bf
computability.DFA: Yes mathlib4#2317 32253a1a1071173b33dc7d6a218cf722c6feb514
computability.NFA: Yes mathlib4#2338 32253a1a1071173b33dc7d6a218cf722c6feb514
computability.ackermann: No mathlib4#2922 9b2660e1b25419042c8da10bf411aa3c67f14383
computability.encoding: No mathlib4#2800 b6395b3a5acd655b16385fa0cdbf1961d6c34b3e
computability.epsilon_NFA: Yes mathlib4#2386 28aa996fc6fb4317f0083c4e6daf79878d81be33
computability.halting: 'No'
computability.language: Yes mathlib4#1453 a239cd3e7ac2c7cde36c913808f9d40c411344f6
computability.partrec: 'No'
computability.partrec_code: 'No'
computability.primrec: No mathlib4#2360 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
computability.reduce: 'No'
computability.regular_expressions: No mathlib4#2306 369525b73f229ccd76a6ec0e0e0bf2be57599768
computability.tm_computable: No mathlib4#2800 6f9cb03e8a39ea345796a13c6639cb330e50869b
computability.tm_to_partrec: 'No'
computability.turing_machine: Yes mathlib4#2125 4c19a16e4b705bf135cf9a80ac18fcc99c438514
control.applicative: Yes mathlib4#798 70d50ecfd4900dd6d328da39ab7ebd516abe4025
control.basic: Yes mathlib4#588 08aeb33b5b693fb1392a7568ae2c0b253516535e
control.bifunctor: Yes mathlib4#2439 dc1525fb3ef6eb4348fb1749c302d8abc303d34a
control.bitraversable.basic: Yes mathlib4#2804 6f1d45dcccf674593073ee4e54da10ba35aedbc0
control.bitraversable.instances: 'No'
control.bitraversable.lemmas: 'No'
control.equiv_functor: Yes mathlib4#649 d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
control.equiv_functor.instances: Yes mathlib4#1613 9003f28797c0664a49e4179487267c494477d853
control.fix: Yes mathlib4#1194 207cfac9fcd06138865b5d04f7091e46d9320432
control.fold: No mathlib4#2341 740acc0e6f9adf4423f92a485d0456fc271482da
control.functor: Yes mathlib4#612 70d50ecfd4900dd6d328da39ab7ebd516abe4025
control.functor.multivariate: Yes mathlib4#1638 008205aa645b3f194c1da47025c5f110c8406eab
control.lawful_fix: Yes mathlib4#1739 1126441d6bccf98c81214a0780c73d499f6721fe
control.monad.basic: Yes mathlib4#752 70d50ecfd4900dd6d328da39ab7ebd516abe4025
control.monad.cont: 'No'
control.monad.writer: No needs control_laws_tac?
control.random: No ad hoc port exists
control.traversable.basic: Yes mathlib4#788 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a
control.traversable.derive: 'No'
control.traversable.equiv: Yes mathlib4#1136 706d88f2b8fdfeb0b22796433d7a6c1a010af9f2
control.traversable.instances: Yes mathlib4#1393 18a5306c091183ac90884daa9373fa3b178e8607
control.traversable.lemmas: Yes mathlib4#948 3342d1b2178381196f818146ff79bc0e7ccd9e2d
control.ulift: Yes mathlib4#638 99e8971dc62f1f7ecf693d75e75fbbabd55849de
control.uliftable: 'No'
data.W.basic: Yes mathlib4#1743 2445c98ae4b87eabebdde552593519b9b6dc350c
data.W.cardinal: Yes mathlib4#2465 6eeb941cf39066417a09b1bbc6e74761cadfcb1a
data.W.constructions: Yes mathlib4#1961 861a26926586cd46ff80264d121cdb6fa0e35cc1
data.analysis.filter: Yes mathlib4#1918 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.analysis.topology: Yes mathlib4#2399 28aa996fc6fb4317f0083c4e6daf79878d81be33
data.array.lemmas: No mathlib4#2194 dde670c9a3f503647fd5bfdf1037bad526d3397a
data.bitvec.basic: No mathlib4#2179 d101e93197bb5f6ea89bd7ba386b7f7dff1f3903
data.bitvec.core: Yes mathlib4#1731 1126441d6bccf98c81214a0780c73d499f6721fe
data.bool.all_any: Yes mathlib4#1357 5a3e819569b0f12cbec59d740a2613018e7b8eec
data.bool.basic: Yes mathlib4#534 c4658a649d216f57e99621708b09dcb3dcccbd23
data.bool.count: Yes mathlib4#1761 8631e2d5ea77f6c13054d9151d82b83069680cb1
data.bool.set: Yes mathlib4#960 ed60ee25ed00d7a62a0d1e5808092e1324cee451
data.bracket: Yes mathlib4#480 c4658a649d216f57e99621708b09dcb3dcccbd23
data.buffer.basic: 'No'
data.buffer.parser.basic: 'No'
data.buffer.parser.numeral: 'No'
data.bundle: Yes mathlib4#1288 9aba7801eeecebb61f58a5763c2b6dd1b47dc6ef
data.char: Yes _ c4658a649d216f57e99621708b09dcb3dcccbd23
data.complex.basic: Yes mathlib4#2718 92ca63f0fb391a9ca5f22d2409a6080e786d99f7
data.complex.cardinality: 'No'
data.complex.determinant: 'No'
data.complex.exponential: Yes mathlib4#2785 372edc36e5d2caafdd135769e0136b5a59186834
data.complex.exponential_bounds: 'No'
data.complex.module: 'No'
data.countable.basic: Yes mathlib4#1787 1f0096e6caa61e9c849ec2adbd227e960e9dff58
data.countable.defs: Yes mathlib4#736 70d50ecfd4900dd6d328da39ab7ebd516abe4025
data.countable.small: Yes mathlib4#1128 bbeb185db4ccee8ed07dc48449414ebfa39cb821
data.dfinsupp.basic: Yes mathlib4#1829 6623e6af705e97002a9054c1c05a980180276fc1
data.dfinsupp.interval: Yes mathlib4#2162 98e83c3d541c77cdb7da20d79611a780ff8e7d90
data.dfinsupp.lex: Yes mathlib4#2199 dde670c9a3f503647fd5bfdf1037bad526d3397a
data.dfinsupp.multiset: Yes mathlib4#2345 740acc0e6f9adf4423f92a485d0456fc271482da
data.dfinsupp.ne_locus: Yes mathlib4#1937 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.dfinsupp.order: Yes mathlib4#1942 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.dfinsupp.well_founded: Yes mathlib4#2944 e9b8651eb1ad354f4de6be35a38ef31efcd2cfaa
data.dlist.basic: Yes mathlib4#616 d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
data.dlist.instances: Yes mathlib4#1932 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.enat.basic: Yes mathlib4#1531 9003f28797c0664a49e4179487267c494477d853
data.enat.lattice: Yes mathlib4#1890 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.erased: Yes mathlib4#937 10b4e499f43088dd3bb7b5796184ad5216648ab1
data.fin.basic: Yes mathlib4#84 008af8bb14b3ebef7e04ec3b0d63b947dee4d26a mathlib4#1084
  ; waiting for backport of algebraic instances on `fin n` to mathlib3 (https://github.com/leanprover-community/mathlib/pull/18107)
data.fin.fin2: Yes mathlib4#478 c4658a649d216f57e99621708b09dcb3dcccbd23
data.fin.interval: Yes mathlib4#1846 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
data.fin.succ_pred: Yes mathlib4#1511 7c523cb78f4153682c2929e3006c863bfef463d0
data.fin.tuple.basic: Yes mathlib4#1516 008205aa645b3f194c1da47025c5f110c8406eab
data.fin.tuple.bubble_sort_induction: Yes mathlib4#2107 4c19a16e4b705bf135cf9a80ac18fcc99c438514
data.fin.tuple.monotone: Yes mathlib4#1827 e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
data.fin.tuple.nat_antidiagonal: Yes mathlib4#2170 98e83c3d541c77cdb7da20d79611a780ff8e7d90
data.fin.tuple.sort: Yes mathlib4#1811 8631e2d5ea77f6c13054d9151d82b83069680cb1
data.fin.vec_notation: Yes mathlib4#1741 2445c98ae4b87eabebdde552593519b9b6dc350c
data.fin_enum: Yes mathlib4#1607 9003f28797c0664a49e4179487267c494477d853
data.finite.basic: Yes mathlib4#1722 1126441d6bccf98c81214a0780c73d499f6721fe
data.finite.card: Yes mathlib4#2183 dde670c9a3f503647fd5bfdf1037bad526d3397a
data.finite.defs: Yes mathlib4#698 a148d797a1094ab554ad4183a4ad6f130358ef64
data.finite.set: Yes mathlib4#1685 509de852e1de55e1efa8eacfa11df0823f26f226
data.finmap: Yes mathlib4#1591 c3fc15b26b3ff8958ec3e5711177a9ae3d5c45b7
data.finset.basic: Yes mathlib4#429 68cc421841f2ebb8ad2b5a35a853895feb4b850a mathlib4#1555
  ; ad hoc port exists
data.finset.card: Yes mathlib4#1589 9003f28797c0664a49e4179487267c494477d853
data.finset.fin: Yes mathlib4#1597 9003f28797c0664a49e4179487267c494477d853
data.finset.finsupp: Yes mathlib4#1990 59694bd07f0a39c5beccba34bd9f413a160782bf
data.finset.fold: Yes mathlib4#1588 9003f28797c0664a49e4179487267c494477d853
data.finset.functor: Yes mathlib4#1974 bcfa726826abd57587355b4b5b7e78ad6527b7e4
data.finset.image: Yes mathlib4#1586 9003f28797c0664a49e4179487267c494477d853
data.finset.interval: No mathlib4#2169 98e83c3d541c77cdb7da20d79611a780ff8e7d90
data.finset.lattice: Yes mathlib4#1606 1c857a1f6798cb054be942199463c2cf904cb937
data.finset.locally_finite: Yes mathlib4#1837 f24cc2891c0e328f0ee8c57387103aa462c44b5e
data.finset.mul_antidiagonal: Yes mathlib4#2158 0a0ec35061ed9960bf0e7ffb0335f44447b58977
data.finset.n_ary: Yes mathlib4#1610 20715f4ac6819ef2453d9e5106ecd086a5dc2a5e
data.finset.nat_antidiagonal: Yes mathlib4#1598 9003f28797c0664a49e4179487267c494477d853
data.finset.noncomm_prod: Yes mathlib4#1681 509de852e1de55e1efa8eacfa11df0823f26f226
data.finset.option: Yes mathlib4#1596 9003f28797c0664a49e4179487267c494477d853
data.finset.order: Yes mathlib4#1584 9003f28797c0664a49e4179487267c494477d853
data.finset.pairwise: Yes mathlib4#1624 9003f28797c0664a49e4179487267c494477d853
data.finset.pi: Yes mathlib4#1590 4c586d291f189eecb9d00581aeb3dd998ac34442
data.finset.pi_induction: Yes mathlib4#1859 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
data.finset.pimage: Yes mathlib4#1965 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.finset.pointwise: Yes mathlib4#1911 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.finset.powerset: Yes mathlib4#1622 9003f28797c0664a49e4179487267c494477d853
data.finset.preimage: Yes mathlib4#1746 2445c98ae4b87eabebdde552593519b9b6dc350c
data.finset.prod: Yes mathlib4#1599 9003f28797c0664a49e4179487267c494477d853
data.finset.sigma: Yes mathlib4#1620 9003f28797c0664a49e4179487267c494477d853
data.finset.slice: Yes mathlib4#1928 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.finset.sort: Yes mathlib4#1675 509de852e1de55e1efa8eacfa11df0823f26f226
data.finset.sum: Yes mathlib4#1601 9003f28797c0664a49e4179487267c494477d853
data.finset.sups: No mathlib4#1663 20715f4ac6819ef2453d9e5106ecd086a5dc2a5e
data.finset.sym: No mathlib4#2361 98e83c3d541c77cdb7da20d79611a780ff8e7d90
data.finsupp.alist: Yes mathlib4#1991 59694bd07f0a39c5beccba34bd9f413a160782bf
data.finsupp.antidiagonal: Yes mathlib4#2142 0a0ec35061ed9960bf0e7ffb0335f44447b58977
data.finsupp.basic: Yes mathlib4#1949 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c Please
  wait for mathlib3#17012
data.finsupp.big_operators: Yes mathlib4#1982 59694bd07f0a39c5beccba34bd9f413a160782bf
data.finsupp.defs: Yes mathlib4#1807 842328d9df7e96fd90fc424e115679c15fb23a71
data.finsupp.fin: Yes mathlib4#1895 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.finsupp.fintype: Yes mathlib4#1936 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.finsupp.indicator: Yes mathlib4#1916 842328d9df7e96fd90fc424e115679c15fb23a71
data.finsupp.interval: Yes mathlib4#2151 0a0ec35061ed9960bf0e7ffb0335f44447b58977
data.finsupp.lex: Yes mathlib4#2272 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
data.finsupp.multiset: Yes mathlib4#1988 59694bd07f0a39c5beccba34bd9f413a160782bf
data.finsupp.ne_locus: Yes mathlib4#1935 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.finsupp.order: Yes mathlib4#1891 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.finsupp.pointwise: Yes mathlib4#1917 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.finsupp.pwo: Yes mathlib4#1989 59694bd07f0a39c5beccba34bd9f413a160782bf
data.finsupp.to_dfinsupp: Yes mathlib4#1995 59694bd07f0a39c5beccba34bd9f413a160782bf
data.finsupp.well_founded: Yes mathlib4#2985 5fd3186f1ec30a75d5f65732e3ce5e623382556f
data.fintype.array: 'No'
data.fintype.basic: Yes mathlib4#429 d78597269638367c3863d40d45108f52207e03cf ad hoc
  port exists
data.fintype.big_operators: Yes mathlib4#1742 2445c98ae4b87eabebdde552593519b9b6dc350c
data.fintype.card: Yes mathlib4#1668 92ca63f0fb391a9ca5f22d2409a6080e786d99f7
data.fintype.card_embedding: Yes mathlib4#2166 98e83c3d541c77cdb7da20d79611a780ff8e7d90
data.fintype.fin: Yes mathlib4#1847 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
data.fintype.lattice: Yes mathlib4#1674 509de852e1de55e1efa8eacfa11df0823f26f226
data.fintype.list: Yes mathlib4#1626 9003f28797c0664a49e4179487267c494477d853
data.fintype.option: Yes mathlib4#1677 509de852e1de55e1efa8eacfa11df0823f26f226
data.fintype.order: Yes mathlib4#1718 1126441d6bccf98c81214a0780c73d499f6721fe
data.fintype.parity: Yes mathlib4#1680 509de852e1de55e1efa8eacfa11df0823f26f226
data.fintype.perm: Yes mathlib4#1691 509de852e1de55e1efa8eacfa11df0823f26f226
data.fintype.pi: Yes mathlib4#1602 9003f28797c0664a49e4179487267c494477d853
data.fintype.powerset: Yes mathlib4#1678 509de852e1de55e1efa8eacfa11df0823f26f226
data.fintype.prod: Yes mathlib4#1676 509de852e1de55e1efa8eacfa11df0823f26f226
data.fintype.quotient: No please wait for [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/quotient.2Elift_on_family/near/286096782)
  to resolve
data.fintype.sigma: Yes mathlib4#1625 9003f28797c0664a49e4179487267c494477d853
data.fintype.small: Yes mathlib4#1703 1126441d6bccf98c81214a0780c73d499f6721fe
data.fintype.sort: Yes mathlib4#1690 509de852e1de55e1efa8eacfa11df0823f26f226
data.fintype.sum: Yes mathlib4#1679 6623e6af705e97002a9054c1c05a980180276fc1
data.fintype.units: Yes mathlib4#1696 509de852e1de55e1efa8eacfa11df0823f26f226
data.fintype.vector: Yes mathlib4#1716 1126441d6bccf98c81214a0780c73d499f6721fe
data.fp.basic: Yes mathlib4#1467 7b78d1776212a91ecc94cf601f83bdcc46b04213
data.fun_like.basic: Yes mathlib4#541 a148d797a1094ab554ad4183a4ad6f130358ef64
data.fun_like.embedding: Yes mathlib4#541 c4658a649d216f57e99621708b09dcb3dcccbd23
data.fun_like.equiv: Yes mathlib4#541 f340f229b1f461aa1c8ee11e0a172d0a3b301a4a
data.fun_like.fintype: Yes mathlib4#1933 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.hash_map: 'No'
data.holor: Yes mathlib4#1669 509de852e1de55e1efa8eacfa11df0823f26f226
data.int.absolute_value: Yes mathlib4#1289 9aba7801eeecebb61f58a5763c2b6dd1b47dc6ef
data.int.associated: Yes mathlib4#1195 207cfac9fcd06138865b5d04f7091e46d9320432
data.int.basic: Yes mathlib4#23 2196ab363eb097c008d4497125e0dde23fb36db2
data.int.bitwise: Yes mathlib4#1159 0743cc5d9d86bcd1bba10f480e948a257d65056f
data.int.cast.basic: Yes mathlib4#641 70d50ecfd4900dd6d328da39ab7ebd516abe4025
data.int.cast.defs: Yes mathlib4#507 99e8971dc62f1f7ecf693d75e75fbbabd55849de
data.int.cast.field: Yes mathlib4#1016 acee671f47b8e7972a1eb6f4eed74b4b3abce829
data.int.cast.lemmas: Yes mathlib4#995 7a89b1aed52bcacbcc4a8ad515e72c5c07268940
data.int.cast.prod: Yes mathlib4#1015 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
data.int.char_zero: Yes mathlib4#1029 acee671f47b8e7972a1eb6f4eed74b4b3abce829
data.int.conditionally_complete_order: Yes mathlib4#1299 1e05171a5e8cf18d98d9cf7b207540acb044acae
data.int.div: Yes mathlib4#1011 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
data.int.dvd.basic: Yes mathlib4#996 e1bccd6e40ae78370f01659715d3c948716e3b7e
data.int.dvd.pow: Yes mathlib4#1087 b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7
data.int.gcd: Yes mathlib4#1183 d4f69d96f3532729da8ebb763f4bc26fcf640f06
data.int.interval: Yes mathlib4#1869 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
data.int.least_greatest: Yes mathlib4#1003 3342d1b2178381196f818146ff79bc0e7ccd9e2d
data.int.lemmas: Yes mathlib4#1271 09597669f02422ed388036273d8848119699c22f
data.int.log: Yes mathlib4#1793 1f0096e6caa61e9c849ec2adbd227e960e9dff58
data.int.modeq: Yes mathlib4#1285 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
data.int.nat_prime: Yes mathlib4#1264 422e70f7ce183d2900c586a8cda8381e788a0c62
data.int.order.basic: Yes mathlib4#584 bd835ef554f37ef9b804f0903089211f89cb370b
data.int.order.lemmas: Yes mathlib4#1002 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
data.int.order.units: Yes mathlib4#1082 d012cd09a9b256d870751284dd6a29882b0be105
data.int.parity: Yes mathlib4#1836 e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
data.int.range: Yes mathlib4#1477 7b78d1776212a91ecc94cf601f83bdcc46b04213
data.int.sqrt: Yes mathlib4#1167 ba2245edf0c8bb155f1569fd9b9492a9b384cde6
data.int.succ_pred: Yes mathlib4#1543 9003f28797c0664a49e4179487267c494477d853
data.int.units: Yes mathlib4#807 641b6a82006416ec431b2987b354af9311fed4f2
data.is_R_or_C.basic: 'No'
data.is_R_or_C.lemmas: 'No'
data.json: 'No'
data.lazy_list: Yes mathlib4#686 41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3
data.lazy_list.basic: Yes mathlib4#1776 1f0096e6caa61e9c849ec2adbd227e960e9dff58
data.list.alist: Yes mathlib4#1530 f808feb6c18afddb25e66a71d317643cf7fb5fbb
data.list.basic: Yes _ 9da1b3534b65d9661eb8f42443598a92bbb49211
data.list.big_operators.basic: Yes mathlib4#1380 6c5f73fd6f6cc83122788a80a27cdd54663609f4
data.list.big_operators.lemmas: Yes mathlib4#1423 f694c7dead66f5d4c80f446c796a5aad14707f0e
data.list.chain: Yes mathlib4#433 dd71334db81d0bd444af1ee339a29298bef40734
data.list.count: Yes mathlib4#1410 6afc9b06856ad973f6a2619e3e8a0a8d537a58f2
data.list.cycle: Yes mathlib4#1642 008205aa645b3f194c1da47025c5f110c8406eab
data.list.dedup: Yes mathlib4#1460 f694c7dead66f5d4c80f446c796a5aad14707f0e
data.list.defs: Yes mathlib4#112 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a
data.list.destutter: Yes mathlib4#1466 7b78d1776212a91ecc94cf601f83bdcc46b04213
data.list.duplicate: Yes mathlib4#1465 f694c7dead66f5d4c80f446c796a5aad14707f0e
data.list.fin_range: Yes mathlib4#1635 9003f28797c0664a49e4179487267c494477d853
data.list.forall2: Yes mathlib4#1359 5a3e819569b0f12cbec59d740a2613018e7b8eec
data.list.func: Yes mathlib4#1048 aba57d4d3dae35460225919dcd82fe91355162f9
data.list.indexes: Yes mathlib4#1812 8631e2d5ea77f6c13054d9151d82b83069680cb1
data.list.infix: Yes mathlib4#1350 26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2
data.list.intervals: No mathlib4#1479 7b78d1776212a91ecc94cf601f83bdcc46b04213
data.list.join: Yes mathlib4#1395 18a5306c091183ac90884daa9373fa3b178e8607
data.list.lattice: Yes mathlib4#1449 dd71334db81d0bd444af1ee339a29298bef40734
data.list.lemmas: Yes mathlib4#1351 975c8c329887c50db6f3556a5f382292ee152ff9
data.list.lex: Yes mathlib4#672 d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
data.list.min_max: Yes mathlib4#1352 6d0adfa76594f304b4650d098273d4366edeb61b
data.list.nat_antidiagonal: Yes mathlib4#1474 7b78d1776212a91ecc94cf601f83bdcc46b04213
data.list.nodup: Yes mathlib4#433 f694c7dead66f5d4c80f446c796a5aad14707f0e
data.list.nodup_equiv_fin: Yes mathlib4#1640 008205aa645b3f194c1da47025c5f110c8406eab
data.list.of_fn: Yes mathlib4#1630 bf27744463e9620ca4e4ebe951fe83530ae6949b Would
  be nice to finish mathlib3#18192 first
data.list.pairwise: Yes mathlib4#429 f694c7dead66f5d4c80f446c796a5aad14707f0e ad hoc
  port exists
data.list.palindrome: Yes mathlib4#1356 5a3e819569b0f12cbec59d740a2613018e7b8eec
data.list.perm: Yes mathlib4#56 7b78d1776212a91ecc94cf601f83bdcc46b04213 mathlib4#1478
  ; WIP @JamesGallicchio
data.list.permutation: Yes mathlib4#1445 dd71334db81d0bd444af1ee339a29298bef40734
data.list.prime: Yes mathlib4#1492 ccad6d5093bd2f5c6ca621fc74674cce51355af6
data.list.prod_sigma: Yes mathlib4#1444 dd71334db81d0bd444af1ee339a29298bef40734
data.list.range: Yes mathlib4#433 7b78d1776212a91ecc94cf601f83bdcc46b04213 mathlib4#1463
  ; ad hoc port exists
data.list.rdrop: Yes mathlib4#1382 26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2
data.list.rotate: Yes mathlib4#1490 ccad6d5093bd2f5c6ca621fc74674cce51355af6
data.list.sections: Yes mathlib4#1381 26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2
data.list.sigma: Yes mathlib4#1493 f808feb6c18afddb25e66a71d317643cf7fb5fbb
data.list.sort: Yes mathlib4#1632 f694c7dead66f5d4c80f446c796a5aad14707f0e
data.list.sublists: Yes mathlib4#1494 ccad6d5093bd2f5c6ca621fc74674cce51355af6
data.list.tfae: Yes mathlib4#1354 5a3e819569b0f12cbec59d740a2613018e7b8eec
data.list.zip: Yes mathlib4#1416 134625f523e737f650a6ea7f0c82a6177e45e622
data.matrix.basic: No mathlib4#2960 21e3562c5e12d846c7def5eff8cdbc520d7d4936 Likely
  to be annoying without leanprover/lean4#2042
data.matrix.basis: 'No'
data.matrix.block: 'No'
data.matrix.char_p: 'No'
data.matrix.dmatrix: Yes mathlib4#1605 9003f28797c0664a49e4179487267c494477d853
data.matrix.dual_number: 'No'
data.matrix.hadamard: 'No'
data.matrix.kronecker: 'No'
data.matrix.notation: 'No'
data.matrix.pequiv: 'No'
data.matrix.rank: 'No'
data.mllist: No mathlib4#2945 8f6fd1b69096c6a587f745d354306c0d46396915 probably not
  needed
data.multiset.antidiagonal: Yes mathlib4#1562 9003f28797c0664a49e4179487267c494477d853
data.multiset.basic: Yes mathlib4#429 f3187269ad18e82a809428a42d6282ce81e4ebcc mathlib4#1491
  ; ad hoc port exists
data.multiset.bind: Yes mathlib4#1537 f694c7dead66f5d4c80f446c796a5aad14707f0e
data.multiset.dedup: Yes mathlib4#1541 9003f28797c0664a49e4179487267c494477d853
data.multiset.finset_ops: Yes mathlib4#1547 9003f28797c0664a49e4179487267c494477d853
data.multiset.fintype: Yes mathlib4#1828 e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
data.multiset.fold: Yes mathlib4#1548 9003f28797c0664a49e4179487267c494477d853
data.multiset.functor: Yes mathlib4#1790 1f0096e6caa61e9c849ec2adbd227e960e9dff58
  mathlib4#1790 ; WIP; `control_laws_tac` would be useful for this
data.multiset.interval: Yes mathlib4#2373 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
data.multiset.lattice: Yes mathlib4#1556 9003f28797c0664a49e4179487267c494477d853
data.multiset.locally_finite: Yes mathlib4#1980 59694bd07f0a39c5beccba34bd9f413a160782bf
data.multiset.nat_antidiagonal: Yes mathlib4#1561 9003f28797c0664a49e4179487267c494477d853
data.multiset.nodup: Yes mathlib4#429 f694c7dead66f5d4c80f446c796a5aad14707f0e ad
  hoc port exists
data.multiset.pi: Yes mathlib4#1551 4c586d291f189eecb9d00581aeb3dd998ac34442
data.multiset.powerset: Yes mathlib4#1544 9003f28797c0664a49e4179487267c494477d853
data.multiset.range: Yes mathlib4#1528 0a0ec35061ed9960bf0e7ffb0335f44447b58977
data.multiset.sections: Yes mathlib4#1554 9003f28797c0664a49e4179487267c494477d853
data.multiset.sort: Yes mathlib4#1639 008205aa645b3f194c1da47025c5f110c8406eab
data.multiset.sum: Yes mathlib4#1546 9003f28797c0664a49e4179487267c494477d853
data.mv_polynomial.basic: Yes mathlib4#2861 2d5739b61641ee4e7e53eca5688a08f66f2e6a60
data.mv_polynomial.cardinal: 'No'
data.mv_polynomial.comap: Yes mathlib4#2904 aba31c938d3243cc671be7091b28a1e0814647ee
data.mv_polynomial.comm_ring: Yes mathlib4#2971 972aa4234fa56ce119d19506045158a9d76881fd
data.mv_polynomial.counit: Yes mathlib4#2900 abb3121f210743a930dea73cd766d988079bdf8b
data.mv_polynomial.derivation: 'No'
data.mv_polynomial.division: 'No'
data.mv_polynomial.equiv: No mathlib4#2997 70fd9563a21e7b963887c9360bd29b2393e6225a
data.mv_polynomial.expand: 'No'
data.mv_polynomial.funext: 'No'
data.mv_polynomial.invertible: Yes mathlib4#2963 f6c030fea3c2809bb489bc8901f307bf6b4bf0c0
data.mv_polynomial.monad: No mathlib4#2887 5120cf49cb659e2499edd7e4d336a04efd598f2f
data.mv_polynomial.pderiv: 'No'
data.mv_polynomial.rename: Yes mathlib4#2886 eabc6192c84ccce3936a8577a987b80b95ba75f6
data.mv_polynomial.supported: Yes mathlib4#2972 a26d17fcd679e43d380d0583b33c9eca5359d41e
data.mv_polynomial.variables: Yes mathlib4#2961 5120cf49cb659e2499edd7e4d336a04efd598f2f
data.nat.basic: Yes _ bd835ef554f37ef9b804f0903089211f89cb370b
data.nat.bits: Yes mathlib4#1095 d012cd09a9b256d870751284dd6a29882b0be105
data.nat.bitwise: Yes mathlib4#1404 6afc9b06856ad973f6a2619e3e8a0a8d537a58f2
data.nat.cast.basic: Yes mathlib4#830 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
data.nat.cast.defs: Yes mathlib4#641 a148d797a1094ab554ad4183a4ad6f130358ef64
data.nat.cast.field: Yes mathlib4#1161 acee671f47b8e7972a1eb6f4eed74b4b3abce829
data.nat.cast.prod: Yes mathlib4#1010 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
data.nat.cast.with_top: Yes mathlib4#1019 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
data.nat.choose.basic: Yes mathlib4#1073 2f3994e1b117b1e1da49bcfb67334f33460c3ce4
data.nat.choose.bounds: Yes mathlib4#1139 550b58538991c8977703fdeb7c9d51a5aa27df11
data.nat.choose.cast: Yes mathlib4#2821 bb168510ef455e9280a152e7f31673cabd3d7496
data.nat.choose.central: Yes mathlib4#2140 0a0ec35061ed9960bf0e7ffb0335f44447b58977
  depends on the decide! tactic
data.nat.choose.dvd: Yes mathlib4#1221 966e0cf0685c9cedf8a3283ac69eef4d5f2eaca2
data.nat.choose.factorization: 'No'
data.nat.choose.multinomial: No mathlib4#2361 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
data.nat.choose.sum: Yes mathlib4#2121 4c19a16e4b705bf135cf9a80ac18fcc99c438514
data.nat.choose.vandermonde: Yes mathlib4#2766 d6814c584384ddf2825ff038e868451a7c956f31
data.nat.count: Yes mathlib4#2209 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
data.nat.digits: Yes mathlib4#2300 369525b73f229ccd76a6ec0e0e0bf2be57599768
data.nat.dist: Yes mathlib4#1023 d50b12ae8e2bd910d08a94823976adae9825718b
data.nat.even_odd_rec: Yes mathlib4#1148 18a5306c091183ac90884daa9373fa3b178e8607
data.nat.factorial.basic: Yes mathlib4#1066 d012cd09a9b256d870751284dd6a29882b0be105
data.nat.factorial.big_operators: Yes mathlib4#1721 1126441d6bccf98c81214a0780c73d499f6721fe
data.nat.factorial.cast: Yes mathlib4#2801 d50b12ae8e2bd910d08a94823976adae9825718b
data.nat.factorization.basic: No mathlib4#3043 f694c7dead66f5d4c80f446c796a5aad14707f0e
data.nat.factorization.prime_pow: 'No'
data.nat.factors: Yes mathlib4#1664 008205aa645b3f194c1da47025c5f110c8406eab
data.nat.fib: Yes mathlib4#1644 008205aa645b3f194c1da47025c5f110c8406eab
data.nat.gcd.basic: Yes mathlib4#1183 a47cda9662ff3925c6df271090b5808adbca5b46
data.nat.gcd.big_operators: Yes mathlib4#1649 008205aa645b3f194c1da47025c5f110c8406eab
data.nat.hyperoperation: Yes mathlib4#1882 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.nat.interval: Yes mathlib4#1838 e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
data.nat.lattice: Yes mathlib4#1751 2445c98ae4b87eabebdde552593519b9b6dc350c
data.nat.log: Yes mathlib4#1089 3e00d81bdcbf77c8188bbd18f5524ddc3ed8cac6
data.nat.modeq: Yes mathlib4#1274 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
data.nat.multiplicity: Yes mathlib4#2974 ceb887ddf3344dab425292e497fa2af91498437c
data.nat.nth: No mathlib4#2297 369525b73f229ccd76a6ec0e0e0bf2be57599768
data.nat.order.basic: Yes mathlib4#907 26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2
data.nat.order.lemmas: Yes mathlib4#927 2258b40dacd2942571c8ce136215350c702dc78f
data.nat.pairing: Yes mathlib4#1172 207cfac9fcd06138865b5d04f7091e46d9320432
data.nat.parity: Yes mathlib4#1661 8631e2d5ea77f6c13054d9151d82b83069680cb1
data.nat.part_enat: Yes mathlib4#1892 114ff8a4a7935cb7531062200bff375e7b1d6d85
data.nat.periodic: Yes mathlib4#2235 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
data.nat.pow: Yes mathlib4#1050 3e00d81bdcbf77c8188bbd18f5524ddc3ed8cac6
data.nat.prime: Yes mathlib4#1156 8631e2d5ea77f6c13054d9151d82b83069680cb1
data.nat.prime_fin: Yes mathlib4#1759 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
data.nat.prime_norm_num: No meta code, do not port directly, instead rewrite the tactic
data.nat.psub: Yes mathlib4#806 70d50ecfd4900dd6d328da39ab7ebd516abe4025
data.nat.set: Yes mathlib4#961 cf9386b56953fb40904843af98b7a80757bbe7f9
data.nat.size: Yes mathlib4#1140 18a5306c091183ac90884daa9373fa3b178e8607
data.nat.sqrt: Yes mathlib4#1142 ba2245edf0c8bb155f1569fd9b9492a9b384cde6
data.nat.sqrt_norm_num: No meta code, do not port directly, instead rewrite the tactic
data.nat.squarefree: 'No'
data.nat.succ_pred: Yes mathlib4#1480 a2d2e18906e2b62627646b5d5be856e6a642062f
data.nat.totient: 'No'
data.nat.units: Yes mathlib4#805 2258b40dacd2942571c8ce136215350c702dc78f
data.nat.upto: Yes mathlib4#1020 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
data.nat.with_bot: Yes mathlib4#1255 966e0cf0685c9cedf8a3283ac69eef4d5f2eaca2
data.num.basic: Yes mathlib4#607 c4658a649d216f57e99621708b09dcb3dcccbd23
data.num.bitwise: Yes mathlib4#1919 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.num.lemmas: No mathlib4#2800 2196ab363eb097c008d4497125e0dde23fb36db2
data.num.prime: 'No'
data.opposite: Yes mathlib4#650 99e8971dc62f1f7ecf693d75e75fbbabd55849de
data.option.basic: Yes mathlib4#137 f340f229b1f461aa1c8ee11e0a172d0a3b301a4a
data.option.defs: Yes mathlib4#137 c4658a649d216f57e99621708b09dcb3dcccbd23
data.option.n_ary: Yes mathlib4#656 995b47e555f1b6297c7cf16855f1023e355219fb
data.ordmap.ordnode: No mathlib4#1455 dd71334db81d0bd444af1ee339a29298bef40734
data.ordmap.ordset: 'No'
data.part: Yes mathlib4#1007 80c43012d26f63026d362c3aba28f3c3bafb07e6
data.pequiv: Yes mathlib4#1008 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
data.pfun: Yes mathlib4#1179 207cfac9fcd06138865b5d04f7091e46d9320432
data.pfunctor.multivariate.M: Yes mathlib4#2362 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
data.pfunctor.multivariate.W: Yes mathlib4#2233 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
data.pfunctor.multivariate.basic: Yes mathlib4#1835 e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
data.pfunctor.univariate.M: Yes mathlib4#1834 8631e2d5ea77f6c13054d9151d82b83069680cb1
data.pfunctor.univariate.basic: Yes mathlib4#1823 8631e2d5ea77f6c13054d9151d82b83069680cb1
data.pi.algebra: Yes mathlib4#564 70d50ecfd4900dd6d328da39ab7ebd516abe4025
data.pi.interval: Yes mathlib4#2177 d101e93197bb5f6ea89bd7ba386b7f7dff1f3903
data.pi.lex: Yes mathlib4#1104 6623e6af705e97002a9054c1c05a980180276fc1
data.pnat.basic: Yes mathlib4#1144 ba2245edf0c8bb155f1569fd9b9492a9b384cde6
data.pnat.defs: Yes mathlib4#604 c4658a649d216f57e99621708b09dcb3dcccbd23
data.pnat.factors: Yes mathlib4#1830 e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
data.pnat.find: Yes mathlib4#1220 207cfac9fcd06138865b5d04f7091e46d9320432
data.pnat.interval: Yes mathlib4#1894 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.pnat.prime: Yes mathlib4#1270 09597669f02422ed388036273d8848119699c22f
data.pnat.xgcd: Yes mathlib4#1408 6afc9b06856ad973f6a2619e3e8a0a8d537a58f2
data.polynomial.algebra_map: Yes mathlib4#2822 e064a7bf82ad94c3c17b5128bbd860d1ec34874e
data.polynomial.basic: Yes mathlib4#2620 1f0096e6caa61e9c849ec2adbd227e960e9dff58
data.polynomial.cancel_leads: Yes mathlib4#2730 70fd9563a21e7b963887c9360bd29b2393e6225a
  Relies on `compute_degree_le` tactic which is not yet implemented
data.polynomial.cardinal: Yes mathlib4#2627 62c0a4ef1441edb463095ea02a06e87f3dfe135c
data.polynomial.coeff: Yes mathlib4#2624 fa256f00ce018e7b40e1dc756e403c86680bf448
data.polynomial.degree.card_pow_degree: 'No'
data.polynomial.degree.definitions: Yes mathlib4#2631 808ea4ebfabeb599f21ec4ae87d6dc969597887f
data.polynomial.degree.lemmas: Yes mathlib4#2723 302eab4f46abb63de520828de78c04cb0f9b5836
data.polynomial.degree.trailing_degree: Yes mathlib4#2722 302eab4f46abb63de520828de78c04cb0f9b5836
data.polynomial.denoms_clearable: Yes mathlib4#2978 85d9f2189d9489f9983c0d01536575b0233bd305
data.polynomial.derivative: Yes mathlib4#2725 bbeb185db4ccee8ed07dc48449414ebfa39cb821
data.polynomial.div: Yes mathlib4#2975 da420a8c6dd5bdfb85c4ced85c34388f633bc6ff
data.polynomial.erase_lead: Yes mathlib4#2721 fa256f00ce018e7b40e1dc756e403c86680bf448
data.polynomial.eval: Yes mathlib4#2645 e064a7bf82ad94c3c17b5128bbd860d1ec34874e
data.polynomial.expand: 'No'
data.polynomial.field_division: No mathlib4#3057 bbeb185db4ccee8ed07dc48449414ebfa39cb821
data.polynomial.hasse_deriv: Yes mathlib4#2842 a148d797a1094ab554ad4183a4ad6f130358ef64
data.polynomial.identities: Yes mathlib4#2914 4e1eeebe63ac6d44585297e89c6e7ee5cbda487a
data.polynomial.induction: Yes mathlib4#2628 63417e01fbc711beaf25fa73b6edb395c0cfddd0
data.polynomial.inductions: Yes mathlib4#2747 70fd9563a21e7b963887c9360bd29b2393e6225a
data.polynomial.integral_normalization: Yes mathlib4#2833 6f401acf4faec3ab9ab13a42789c4f68064a61cd
data.polynomial.laurent: No mathlib4#2953 831c494092374cfe9f50591ed0ac81a25efc5b86
data.polynomial.lifts: Yes mathlib4#2835 63417e01fbc711beaf25fa73b6edb395c0cfddd0
data.polynomial.mirror: 'No'
data.polynomial.module: 'No'
data.polynomial.monic: Yes mathlib4#2745 cbdf7b565832144d024caa5a550117c6df0204a5
data.polynomial.monomial: Yes mathlib4#2623 220f71ba506c8958c9b41bd82226b3d06b0991e8
data.polynomial.partial_fractions: 'No'
data.polynomial.reverse: Yes mathlib4#2729 44de64f183393284a16016dfb2a48ac97382f2bd
data.polynomial.ring_division: Yes mathlib4#3029 cbdf7b565832144d024caa5a550117c6df0204a5
data.polynomial.splits: 'No'
data.polynomial.taylor: Yes mathlib4#2850 70fd9563a21e7b963887c9360bd29b2393e6225a
data.polynomial.unit_trinomial: 'No'
data.prod.basic: Yes mathlib4#545 bd9851ca476957ea4549eb19b40e7b5ade9428cc
data.prod.lex: Yes mathlib4#783 70d50ecfd4900dd6d328da39ab7ebd516abe4025
data.prod.pprod: Yes mathlib4#496 c4658a649d216f57e99621708b09dcb3dcccbd23
data.prod.tprod: Yes mathlib4#1464 7b78d1776212a91ecc94cf601f83bdcc46b04213
data.psigma.order: Yes mathlib4#815 62a5626868683c104774de8d85b9855234ac807c
data.qpf.multivariate.basic: Yes mathlib4#2223 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
data.qpf.multivariate.constructions.cofix: No mathlib4#2444 f694c7dead66f5d4c80f446c796a5aad14707f0e
data.qpf.multivariate.constructions.comp: Yes mathlib4#2228 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
data.qpf.multivariate.constructions.const: Yes mathlib4#2224 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
data.qpf.multivariate.constructions.fix: Yes mathlib4#2409 28aa996fc6fb4317f0083c4e6daf79878d81be33
data.qpf.multivariate.constructions.prj: Yes mathlib4#2226 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
data.qpf.multivariate.constructions.quot: Yes mathlib4#2227 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
data.qpf.multivariate.constructions.sigma: Yes mathlib4#2225 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
data.qpf.univariate.basic: 'No'
data.quot: Yes mathlib4#559 6ed6abbde29b8f630001a1b481603f657a3384f1
data.rat.basic: Yes mathlib4#998 a59dad53320b73ef180174aae867addd707ef00e
data.rat.big_operators: Yes mathlib4#1660 008205aa645b3f194c1da47025c5f110c8406eab
data.rat.cast: Yes mathlib4#1261 422e70f7ce183d2900c586a8cda8381e788a0c62
data.rat.defs: Yes mathlib4#733 18a5306c091183ac90884daa9373fa3b178e8607
data.rat.denumerable: Yes mathlib4#2197 dde670c9a3f503647fd5bfdf1037bad526d3397a
data.rat.encodable: Yes mathlib4#1569 9003f28797c0664a49e4179487267c494477d853
data.rat.floor: Yes mathlib4#1418 e1bccd6e40ae78370f01659715d3c948716e3b7e
data.rat.init: Yes mathlib4#695 f340f229b1f461aa1c8ee11e0a172d0a3b301a4a
data.rat.lemmas: Yes mathlib4#1138 550b58538991c8977703fdeb7c9d51a5aa27df11
data.rat.meta_defs: 'No'
data.rat.nnrat: Yes mathlib4#2392 b3f4f007a962e3787aa0f3b5c7942a1317f7d88e
data.rat.order: Yes mathlib4#733 a59dad53320b73ef180174aae867addd707ef00e
data.rat.sqrt: Yes mathlib4#1252 46a64b5b4268c594af770c44d9e502afc6a515cb
data.rbmap.basic: No WIP @digama0
data.rbmap.default: No WIP @digama0 do not port default files
data.rbtree.basic: No WIP @digama0
data.rbtree.default_lt: No WIP @digama0
data.rbtree.find: No WIP @digama0
data.rbtree.init: No WIP @digama0
data.rbtree.insert: No WIP @digama0
data.rbtree.main: No WIP @digama0
data.rbtree.min_max: No WIP @digama0
data.real.basic: Yes mathlib4#1514 7c523cb78f4153682c2929e3006c863bfef463d0
data.real.cardinality: 'No'
data.real.cau_seq: Yes mathlib4#1124 9116dd6709f303dcf781632e15fdef382b0fc579
data.real.cau_seq_completion: Yes mathlib4#1440 40acfb6aa7516ffe6f91136691df012a64683390
data.real.conjugate_exponents: Yes mathlib4#2411 2196ab363eb097c008d4497125e0dde23fb36db2
data.real.enat_ennreal: Yes mathlib4#2529 53b216bcc1146df1c4a0a86877890ea9f1f01589
data.real.ennreal: Yes mathlib4#2388 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
data.real.ereal: Yes mathlib4#2501 2196ab363eb097c008d4497125e0dde23fb36db2 please
  wait for mathlib#18481
data.real.golden_ratio: 'No'
data.real.hyperreal: 'No'
data.real.irrational: 'No'
data.real.nnreal: Yes mathlib4#2234 b3f4f007a962e3787aa0f3b5c7942a1317f7d88e
data.real.pi.bounds: 'No'
data.real.pi.leibniz: 'No'
data.real.pi.wallis: 'No'
data.real.pointwise: Yes mathlib4#2196 dde670c9a3f503647fd5bfdf1037bad526d3397a
data.real.sign: Yes mathlib4#1618 9003f28797c0664a49e4179487267c494477d853
data.real.sqrt: Yes mathlib4#2674 f2ce6086713c78a7f880485f7917ea547a215982
data.rel: Yes mathlib4#1134 706d88f2b8fdfeb0b22796433d7a6c1a010af9f2
data.semiquot: Yes mathlib4#1275 09597669f02422ed388036273d8848119699c22f
data.seq.computation: Yes mathlib4#1216 1f0096e6caa61e9c849ec2adbd227e960e9dff58
data.seq.parallel: 'No'
data.seq.seq: No mathlib4#1808 8631e2d5ea77f6c13054d9151d82b83069680cb1 merge mathlib#18284
  first
data.seq.wseq: 'No'
data.set.Union_lift: Yes mathlib4#1193 207cfac9fcd06138865b5d04f7091e46d9320432
data.set.accumulate: Yes mathlib4#1210 207cfac9fcd06138865b5d04f7091e46d9320432
data.set.basic: Yes mathlib4#892 75608affb24b4f48699fbcd38f227827f7793771
data.set.bool_indicator: Yes mathlib4#988 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
data.set.constructions: Yes mathlib4#1585 9003f28797c0664a49e4179487267c494477d853
data.set.countable: Yes mathlib4#1788 1f0096e6caa61e9c849ec2adbd227e960e9dff58
data.set.enumerate: Yes mathlib4#1041 92ca63f0fb391a9ca5f22d2409a6080e786d99f7
data.set.equitable: Yes mathlib4#1809 8631e2d5ea77f6c13054d9151d82b83069680cb1
data.set.finite: Yes mathlib4#1734 1f0096e6caa61e9c849ec2adbd227e960e9dff58
data.set.function: Yes mathlib4#1035 996b0ff959da753a555053a480f36e5f264d4207
data.set.functor: Yes mathlib4#1178 207cfac9fcd06138865b5d04f7091e46d9320432
data.set.image: Yes mathlib4#949 4550138052d0a416b700c27056d492e2ef53214e
data.set.intervals.basic: Yes mathlib4#1033 198161d833f2c01498c39c266b0b3dbe2c7a8c07
data.set.intervals.disjoint: Yes mathlib4#1198 207cfac9fcd06138865b5d04f7091e46d9320432
data.set.intervals.group: Yes mathlib4#1038 740acc0e6f9adf4423f92a485d0456fc271482da
data.set.intervals.infinite: Yes mathlib4#1792 1f0096e6caa61e9c849ec2adbd227e960e9dff58
data.set.intervals.instances: Yes mathlib4#1068 d012cd09a9b256d870751284dd6a29882b0be105
data.set.intervals.iso_Ioo: Yes mathlib4#1321 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
data.set.intervals.monoid: Yes mathlib4#1039 aba57d4d3dae35460225919dcd82fe91355162f9
data.set.intervals.monotone: Yes mathlib4#1294 9aba7801eeecebb61f58a5763c2b6dd1b47dc6ef
data.set.intervals.ord_connected: Yes mathlib4#1186 9003f28797c0664a49e4179487267c494477d853
data.set.intervals.ord_connected_component: Yes mathlib4#1303 92ca63f0fb391a9ca5f22d2409a6080e786d99f7
data.set.intervals.order_iso: Yes mathlib4#1067 d012cd09a9b256d870751284dd6a29882b0be105
data.set.intervals.pi: Yes mathlib4#1223 207cfac9fcd06138865b5d04f7091e46d9320432
data.set.intervals.proj_Icc: Yes mathlib4#1051 aba57d4d3dae35460225919dcd82fe91355162f9
data.set.intervals.surj_on: Yes mathlib4#1064 a59dad53320b73ef180174aae867addd707ef00e
data.set.intervals.unordered_interval: Yes mathlib4#1062 9003f28797c0664a49e4179487267c494477d853
data.set.intervals.with_bot_top: Yes mathlib4#1072 d012cd09a9b256d870751284dd6a29882b0be105
data.set.lattice: Yes mathlib4#1121 b86832321b586c6ac23ef8cdef6a7a27e42b13bd
data.set.mul_antidiagonal: Yes mathlib4#2152 0a0ec35061ed9960bf0e7ffb0335f44447b58977
data.set.n_ary: Yes mathlib4#969 20715f4ac6819ef2453d9e5106ecd086a5dc2a5e
data.set.opposite: Yes mathlib4#983 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
data.set.pairwise: Yes mathlib4#1175 207cfac9fcd06138865b5d04f7091e46d9320432
data.set.pointwise.basic: Yes mathlib4#1188 207cfac9fcd06138865b5d04f7091e46d9320432
data.set.pointwise.big_operators: Yes mathlib4#1651 008205aa645b3f194c1da47025c5f110c8406eab
data.set.pointwise.finite: Yes mathlib4#1844 0a0ec35061ed9960bf0e7ffb0335f44447b58977
data.set.pointwise.interval: Yes mathlib4#1481 2196ab363eb097c008d4497125e0dde23fb36db2
data.set.pointwise.iterate: Yes mathlib4#1563 9003f28797c0664a49e4179487267c494477d853
data.set.pointwise.list_of_fn: Yes mathlib4#1634 f694c7dead66f5d4c80f446c796a5aad14707f0e
data.set.pointwise.smul: Yes mathlib4#1473 7b78d1776212a91ecc94cf601f83bdcc46b04213
  Only minor fixes to to_additive required
data.set.pointwise.support: Yes mathlib4#1915 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
data.set.prod: Yes mathlib4#1004 27f315c5591c84687852f816d8ef31fe103d03de
data.set.semiring: Yes mathlib4#1535 62e8311c791f02c47451bf14aa2501048e7c2f33
data.set.sigma: Yes mathlib4#982 2258b40dacd2942571c8ce136215350c702dc78f
data.set.sups: Yes mathlib4#2991 20715f4ac6819ef2453d9e5106ecd086a5dc2a5e
data.set_like.basic: Yes mathlib4#993 feb99064803fd3108e37c18b0f77d0a8344677a3
data.set_like.fintype: Yes mathlib4#1727 1126441d6bccf98c81214a0780c73d499f6721fe
data.setoid.basic: Yes mathlib4#1117 bbeb185db4ccee8ed07dc48449414ebfa39cb821
data.setoid.partition: Yes mathlib4#2066 b363547b3113d350d053abdf2884e9850a56b205
data.sigma.basic: Yes mathlib4#479 a148d797a1094ab554ad4183a4ad6f130358ef64
data.sigma.interval: Yes mathlib4#2114 4c19a16e4b705bf135cf9a80ac18fcc99c438514
data.sigma.lex: Yes mathlib4#646 41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3
data.sigma.order: Yes mathlib4#887 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a
data.sign: Yes mathlib4#1744 2445c98ae4b87eabebdde552593519b9b6dc350c
data.stream.defs: Yes mathlib4#665 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3
data.stream.init: Yes mathlib4#849 207cfac9fcd06138865b5d04f7091e46d9320432
data.string.basic: No mathlib4#1054 ; WIP @chabulhwi
data.string.defs: No ad hoc port exists
data.subtype: Yes mathlib4#29 c4658a649d216f57e99621708b09dcb3dcccbd23
data.sum.basic: Yes mathlib4#497 bd9851ca476957ea4549eb19b40e7b5ade9428cc
data.sum.interval: Yes mathlib4#1962 861a26926586cd46ff80264d121cdb6fa0e35cc1
data.sum.order: Yes mathlib4#880 f1a2caaf51ef593799107fe9a8d5e411599f3996
data.sym.basic: Yes mathlib4#1672 509de852e1de55e1efa8eacfa11df0823f26f226
data.sym.card: 'No'
data.sym.sym2: Yes mathlib4#1805 8631e2d5ea77f6c13054d9151d82b83069680cb1
data.tree: Yes mathlib4#2587 ed989ff568099019c6533a4d94b27d852a5710d8
data.two_pointing: Yes mathlib4#984 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
data.typevec: Yes mathlib4#891 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3
data.ulift: Yes mathlib4#703 41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3
data.vector.basic: Yes mathlib4#1633 f694c7dead66f5d4c80f446c796a5aad14707f0e
data.vector.mem: Yes mathlib4#1697 509de852e1de55e1efa8eacfa11df0823f26f226
data.vector.zip: Yes mathlib4#1705 1126441d6bccf98c81214a0780c73d499f6721fe
data.vector3: No mathlib4#1204 207cfac9fcd06138865b5d04f7091e46d9320432
data.zmod.algebra: Yes mathlib4#2990 972aa4234fa56ce119d19506045158a9d76881fd
data.zmod.basic: Yes mathlib4#2870 297619ec79dedf23525458b6bf5bf35c736fd2b8
data.zmod.coprime: Yes mathlib4#3019 4b4975cf92a1ffe2ddfeff6ff91b0c46a9162bf5
data.zmod.defs: Yes mathlib4#1713 1126441d6bccf98c81214a0780c73d499f6721fe
data.zmod.parity: Yes mathlib4#2893 048240e809f04e2bde02482ab44bc230744cc6c9
data.zmod.quotient: 'No'
deprecated.group: Yes mathlib4#1368 5a3e819569b0f12cbec59d740a2613018e7b8eec
deprecated.ring: Yes mathlib4#1368 5a3e819569b0f12cbec59d740a2613018e7b8eec
deprecated.subfield: Yes mathlib4#2410 bd9851ca476957ea4549eb19b40e7b5ade9428cc
deprecated.subgroup: Yes mathlib4#1876 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
deprecated.submonoid: Yes mathlib4#1666 509de852e1de55e1efa8eacfa11df0823f26f226
deprecated.subring: Yes mathlib4#2355 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
dynamics.circle.rotation_number.translation_number: 'No'
dynamics.ergodic.add_circle: 'No'
dynamics.ergodic.conservative: 'No'
dynamics.ergodic.ergodic: 'No'
dynamics.ergodic.measure_preserving: 'No'
dynamics.fixed_points.basic: Yes mathlib4#1131 b86832321b586c6ac23ef8cdef6a7a27e42b13bd
dynamics.fixed_points.topology: Yes mathlib4#2023 d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
dynamics.flow: Yes mathlib4#2451 717c073262cd9d59b1a1dcda7e8ab570c5b63370
dynamics.minimal: Yes mathlib4#2075 4c19a16e4b705bf135cf9a80ac18fcc99c438514
dynamics.omega_limit: Yes mathlib4#2490 f2ce6086713c78a7f880485f7917ea547a215982
dynamics.periodic_pts: Yes mathlib4#1887 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
field_theory.abel_ruffini: 'No'
field_theory.adjoin: 'No'
field_theory.cardinality: 'No'
field_theory.chevalley_warning: 'No'
field_theory.finite.basic: 'No'
field_theory.finite.galois_field: 'No'
field_theory.finite.polynomial: 'No'
field_theory.finite.trace: 'No'
field_theory.finiteness: 'No'
field_theory.fixed: 'No'
field_theory.galois: 'No'
field_theory.intermediate_field: 'No'
field_theory.is_alg_closed.algebraic_closure: 'No'
field_theory.is_alg_closed.basic: 'No'
field_theory.is_alg_closed.classification: 'No'
field_theory.krull_topology: 'No'
field_theory.laurent: 'No'
field_theory.minpoly.basic: 'No'
field_theory.minpoly.field: 'No'
field_theory.minpoly.is_integrally_closed: 'No'
field_theory.mv_polynomial: 'No'
field_theory.normal: 'No'
field_theory.perfect_closure: Yes mathlib4#2879 70fd9563a21e7b963887c9360bd29b2393e6225a
field_theory.polynomial_galois_group: 'No'
field_theory.primitive_element: 'No'
field_theory.ratfunc: 'No'
field_theory.separable: 'No'
field_theory.separable_degree: 'No'
field_theory.splitting_field: 'No'
field_theory.subfield: Yes mathlib4#2395 28aa996fc6fb4317f0083c4e6daf79878d81be33
field_theory.tower: 'No'
geometry.euclidean.angle.oriented.affine: 'No'
geometry.euclidean.angle.oriented.basic: 'No'
geometry.euclidean.angle.oriented.right_angle: 'No'
geometry.euclidean.angle.oriented.rotation: 'No'
geometry.euclidean.angle.sphere: 'No'
geometry.euclidean.angle.unoriented.affine: 'No'
geometry.euclidean.angle.unoriented.basic: 'No'
geometry.euclidean.angle.unoriented.conformal: 'No'
geometry.euclidean.angle.unoriented.right_angle: 'No'
geometry.euclidean.basic: 'No'
geometry.euclidean.circumcenter: 'No'
geometry.euclidean.inversion: 'No'
geometry.euclidean.monge_point: 'No'
geometry.euclidean.sphere.basic: 'No'
geometry.euclidean.sphere.power: 'No'
geometry.euclidean.sphere.ptolemy: 'No'
geometry.euclidean.sphere.second_inter: 'No'
geometry.euclidean.triangle: 'No'
geometry.manifold.algebra.left_invariant_derivation: 'No'
geometry.manifold.algebra.lie_group: 'No'
geometry.manifold.algebra.monoid: 'No'
geometry.manifold.algebra.smooth_functions: 'No'
geometry.manifold.algebra.structures: 'No'
geometry.manifold.bump_function: 'No'
geometry.manifold.charted_space: No mathlib4#2365 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
geometry.manifold.complex: 'No'
geometry.manifold.conformal_groupoid: 'No'
geometry.manifold.cont_mdiff: 'No'
geometry.manifold.cont_mdiff_map: 'No'
geometry.manifold.cont_mdiff_mfderiv: 'No'
geometry.manifold.derivation_bundle: 'No'
geometry.manifold.diffeomorph: 'No'
geometry.manifold.instances.real: 'No'
geometry.manifold.instances.sphere: 'No'
geometry.manifold.instances.units_of_normed_algebra: 'No'
geometry.manifold.local_invariant_properties: 'No'
geometry.manifold.metrizable: 'No'
geometry.manifold.mfderiv: 'No'
geometry.manifold.partition_of_unity: 'No'
geometry.manifold.smooth_manifold_with_corners: 'No'
geometry.manifold.tangent_bundle: 'No'
geometry.manifold.vector_bundle.basic: 'No'
geometry.manifold.vector_bundle.fiberwise_linear: 'No'
geometry.manifold.vector_bundle.pullback: 'No'
geometry.manifold.vector_bundle.tangent: 'No'
geometry.manifold.whitney_embedding: 'No'
group_theory.abelianization: Yes mathlib4#2215 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
group_theory.archimedean: Yes mathlib4#1856 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
group_theory.commensurable: Yes mathlib4#2293 48085f140e684306f9e7da907cd5932056d1aded
group_theory.commutator: Yes mathlib4#2143 0a0ec35061ed9960bf0e7ffb0335f44447b58977
group_theory.commuting_probability: Yes mathlib4#2284 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
group_theory.complement: 'No'
group_theory.congruence: Yes mathlib4#1316 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
group_theory.coset: Yes mathlib4#1874 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
group_theory.divisible: Yes mathlib4#2149 0a0ec35061ed9960bf0e7ffb0335f44447b58977
group_theory.double_coset: Yes mathlib4#2076 4c19a16e4b705bf135cf9a80ac18fcc99c438514
group_theory.eckmann_hilton: Yes mathlib4#626 41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3
group_theory.exponent: 'No'
group_theory.finite_abelian: 'No'
group_theory.finiteness: Yes mathlib4#2187 dde670c9a3f503647fd5bfdf1037bad526d3397a
group_theory.free_abelian_group: Yes mathlib4#2247 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
group_theory.free_abelian_group_finsupp: 'No'
group_theory.free_group: Yes mathlib4#1867 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
group_theory.free_product: No mathlib4#2979 9114ddffa023340c9ec86965e00cdd6fe26fcdf6
group_theory.group_action.basic: Yes mathlib4#1845 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
group_theory.group_action.big_operators: Yes mathlib4#1655 008205aa645b3f194c1da47025c5f110c8406eab
group_theory.group_action.conj_act: Yes mathlib4#1871 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
group_theory.group_action.defs: Yes mathlib4#854 dad7ecf9a1feae63e6e49f07619b7087403fb8d4
group_theory.group_action.embedding: Yes mathlib4#1277 a437a2499163d85d670479f69f625f461cc5fef9
group_theory.group_action.fixing_subgroup: Yes mathlib4#1868 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
group_theory.group_action.group: Yes mathlib4#1146 ba2245edf0c8bb155f1569fd9b9492a9b384cde6
group_theory.group_action.opposite: Yes mathlib4#1001 4330aae21f538b862f8aead371cfb6ee556398f1
group_theory.group_action.option: Yes mathlib4#884 f1a2caaf51ef593799107fe9a8d5e411599f3996
group_theory.group_action.pi: Yes mathlib4#1115 bbeb185db4ccee8ed07dc48449414ebfa39cb821
group_theory.group_action.prod: Yes mathlib4#1056 aba57d4d3dae35460225919dcd82fe91355162f9
group_theory.group_action.quotient: Yes mathlib4#2213 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
group_theory.group_action.sigma: Yes mathlib4#885 f1a2caaf51ef593799107fe9a8d5e411599f3996
group_theory.group_action.sub_mul_action: Yes mathlib4#1872 feb99064803fd3108e37c18b0f77d0a8344677a3
group_theory.group_action.sub_mul_action.pointwise: Yes mathlib4#1893 2bbc7e3884ba234309d2a43b19144105a753292e
group_theory.group_action.sum: Yes mathlib4#882 f1a2caaf51ef593799107fe9a8d5e411599f3996
group_theory.group_action.support: Yes mathlib4#1560 9003f28797c0664a49e4179487267c494477d853
group_theory.group_action.units: Yes mathlib4#878 f1a2caaf51ef593799107fe9a8d5e411599f3996
group_theory.index: Yes mathlib4#2222 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
group_theory.is_free_group: Yes mathlib4#1889 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
group_theory.monoid_localization: Yes mathlib4#1777 1f0096e6caa61e9c849ec2adbd227e960e9dff58
group_theory.nielsen_schreier: 'No'
group_theory.nilpotent: 'No'
group_theory.noncomm_pi_coprod: Yes mathlib4#2449 6f9f36364eae3f42368b04858fd66d6d9ae730d8
group_theory.order_of_element: Yes mathlib4#2279 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
group_theory.p_group: 'No'
group_theory.perm.basic: Yes mathlib4#1105 b86832321b586c6ac23ef8cdef6a7a27e42b13bd
group_theory.perm.cycle.basic: Yes mathlib4#2528 92ca63f0fb391a9ca5f22d2409a6080e786d99f7
group_theory.perm.cycle.concrete: 'No'
group_theory.perm.cycle.type: No mathlib4#3027 47adfab39a11a072db552f47594bf8ed2cf8a722
group_theory.perm.fin: 'No'
group_theory.perm.list: Yes mathlib4#1631 9003f28797c0664a49e4179487267c494477d853
group_theory.perm.option: Yes mathlib4#2523 c3019c79074b0619edb4b27553a91b2e82242395
group_theory.perm.sign: Yes mathlib4#2458 f694c7dead66f5d4c80f446c796a5aad14707f0e
group_theory.perm.subgroup: Yes mathlib4#2086 4c19a16e4b705bf135cf9a80ac18fcc99c438514
group_theory.perm.support: Yes mathlib4#1614 9003f28797c0664a49e4179487267c494477d853
group_theory.perm.via_embedding: Yes mathlib4#1163 9116dd6709f303dcf781632e15fdef382b0fc579
group_theory.presented_group: Yes mathlib4#2010 d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
group_theory.quotient_group: Yes mathlib4#1996 59694bd07f0a39c5beccba34bd9f413a160782bf
group_theory.schreier: 'No'
group_theory.schur_zassenhaus: 'No'
group_theory.semidirect_product: Yes mathlib4#1878 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
group_theory.solvable: Yes mathlib4#2221 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
group_theory.specific_groups.alternating: 'No'
group_theory.specific_groups.cyclic: 'No'
group_theory.specific_groups.dihedral: 'No'
group_theory.specific_groups.quaternion: 'No'
group_theory.subgroup.actions: Yes mathlib4#1850 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
group_theory.subgroup.basic: Yes mathlib4#1797 c10e724be91096453ee3db13862b9fb9a992fef2
group_theory.subgroup.finite: Yes mathlib4#1864 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
group_theory.subgroup.mul_opposite: Yes mathlib4#1857 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
group_theory.subgroup.pointwise: Yes mathlib4#1981 c10e724be91096453ee3db13862b9fb9a992fef2
group_theory.subgroup.saturated: Yes mathlib4#1884 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
group_theory.subgroup.simple: Yes mathlib4#1858 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
group_theory.subgroup.zpowers: Yes mathlib4#1852 f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
group_theory.submonoid.basic: Yes mathlib4#1224 feb99064803fd3108e37c18b0f77d0a8344677a3
group_theory.submonoid.center: Yes mathlib4#1315 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
group_theory.submonoid.centralizer: Yes mathlib4#1324 44b58b42794e5abe2bf86397c38e26b587e07e59
group_theory.submonoid.inverses: Yes mathlib4#1987 59694bd07f0a39c5beccba34bd9f413a160782bf
group_theory.submonoid.membership: Yes mathlib4#1699 509de852e1de55e1efa8eacfa11df0823f26f226
group_theory.submonoid.operations: Yes mathlib4#1281 cf8e77c636317b059a8ce20807a29cf3772a0640
group_theory.submonoid.pointwise: Yes mathlib4#1977 2bbc7e3884ba234309d2a43b19144105a753292e
group_theory.subsemigroup.basic: Yes mathlib4#1180 feb99064803fd3108e37c18b0f77d0a8344677a3
group_theory.subsemigroup.center: Yes mathlib4#1278 a437a2499163d85d670479f69f625f461cc5fef9
group_theory.subsemigroup.centralizer: Yes mathlib4#1286 ffc3730d545623aedf5d5bd46a3153cbf41f6c2c
group_theory.subsemigroup.membership: Yes mathlib4#1318 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
group_theory.subsemigroup.operations: Yes mathlib4#1235 207cfac9fcd06138865b5d04f7091e46d9320432
group_theory.sylow: 'No'
group_theory.torsion: 'No'
group_theory.transfer: 'No'
information_theory.hamming: No mathlib4#2891 17ef379e997badd73e5eabb4d38f11919ab3c4b3
lean_core.data.buffer.parser: 'No'
lean_core.data.dlist: No Waiting on tactic abstract
lean_core.data.vector: Yes mathlib4#834 _
linear_algebra.adic_completion: 'No'
linear_algebra.affine_space.affine_equiv: Yes mathlib4#2692 bd1fc183335ea95a9519a1630bcf901fe9326d83
linear_algebra.affine_space.affine_map: Yes mathlib4#2570 bd1fc183335ea95a9519a1630bcf901fe9326d83
linear_algebra.affine_space.affine_subspace: No mathlib4#3051 e96bdfbd1e8c98a09ff75f7ac6204d142debc840
linear_algebra.affine_space.basic: Yes mathlib4#2165 98e83c3d541c77cdb7da20d79611a780ff8e7d90
linear_algebra.affine_space.basis: 'No'
linear_algebra.affine_space.combination: No mathlib4#3051 87c54600fe3cdc7d32ff5b50873ac724d86aef8d
linear_algebra.affine_space.finite_dimensional: 'No'
linear_algebra.affine_space.independent: 'No'
linear_algebra.affine_space.matrix: 'No'
linear_algebra.affine_space.midpoint: No mathlib4#3050 2196ab363eb097c008d4497125e0dde23fb36db2
linear_algebra.affine_space.midpoint_zero: 'No'
linear_algebra.affine_space.ordered: 'No'
linear_algebra.affine_space.pointwise: 'No'
linear_algebra.affine_space.restrict: 'No'
linear_algebra.affine_space.slope: Yes mathlib4#2728 70fd9563a21e7b963887c9360bd29b2393e6225a
linear_algebra.alternating: 'No'
linear_algebra.annihilating_polynomial: 'No'
linear_algebra.basic: Yes mathlib4#1979 b363547b3113d350d053abdf2884e9850a56b205
linear_algebra.basis: Yes mathlib4#2435 2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e
linear_algebra.basis.bilinear: Yes mathlib4#2546 87c54600fe3cdc7d32ff5b50873ac724d86aef8d
linear_algebra.bilinear_form: 'No'
linear_algebra.bilinear_form.tensor_product: 'No'
linear_algebra.bilinear_map: Yes mathlib4#2434 87c54600fe3cdc7d32ff5b50873ac724d86aef8d
linear_algebra.charpoly.basic: 'No'
linear_algebra.charpoly.to_matrix: 'No'
linear_algebra.clifford_algebra.basic: 'No'
linear_algebra.clifford_algebra.conjugation: 'No'
linear_algebra.clifford_algebra.contraction: 'No'
linear_algebra.clifford_algebra.equivs: 'No'
linear_algebra.clifford_algebra.even: 'No'
linear_algebra.clifford_algebra.even_equiv: 'No'
linear_algebra.clifford_algebra.fold: 'No'
linear_algebra.clifford_algebra.grading: 'No'
linear_algebra.clifford_algebra.star: 'No'
linear_algebra.coevaluation: 'No'
linear_algebra.contraction: 'No'
linear_algebra.cross_product: 'No'
linear_algebra.determinant: 'No'
linear_algebra.dfinsupp: Yes mathlib4#2550 a148d797a1094ab554ad4183a4ad6f130358ef64
linear_algebra.dimension: 'No'
linear_algebra.direct_sum.finsupp: 'No'
linear_algebra.direct_sum.tensor_product: No mathlib4#2977 9b9d125b7be0930f564a68f1d73ace10cf46064d
linear_algebra.dual: 'No'
linear_algebra.eigenspace: 'No'
linear_algebra.exterior_algebra.basic: 'No'
linear_algebra.exterior_algebra.grading: 'No'
linear_algebra.exterior_algebra.of_alternating: 'No'
linear_algebra.finite_dimensional: 'No'
linear_algebra.finrank: 'No'
linear_algebra.finsupp: Yes mathlib4#2277 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
linear_algebra.finsupp_vector_space: 'No'
linear_algebra.free_algebra: 'No'
linear_algebra.free_module.basic: 'No'
linear_algebra.free_module.determinant: 'No'
linear_algebra.free_module.finite.basic: 'No'
linear_algebra.free_module.finite.matrix: 'No'
linear_algebra.free_module.finite.rank: 'No'
linear_algebra.free_module.ideal_quotient: 'No'
linear_algebra.free_module.pid: 'No'
linear_algebra.free_module.rank: 'No'
linear_algebra.free_module.strong_rank_condition: 'No'
linear_algebra.general_linear_group: Yes mathlib4#2035 2705404e701abc6b3127da906f40bae062a169c9
linear_algebra.invariant_basis_number: Yes mathlib4#3025 5fd3186f1ec30a75d5f65732e3ce5e623382556f
linear_algebra.isomorphisms: No mathlib4#2364 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
linear_algebra.lagrange: 'No'
linear_algebra.linear_independent: Yes mathlib4#2436 6d584f1709bedbed9175bd9350df46599bdd7213
linear_algebra.linear_pmap: Yes mathlib4#2422 8709a597a377df3433d863887978b3d01a07c587
linear_algebra.matrix.absolute_value: 'No'
linear_algebra.matrix.adjugate: 'No'
linear_algebra.matrix.basis: 'No'
linear_algebra.matrix.bilinear_form: 'No'
linear_algebra.matrix.block: 'No'
linear_algebra.matrix.charpoly.basic: 'No'
linear_algebra.matrix.charpoly.coeff: 'No'
linear_algebra.matrix.charpoly.finite_field: 'No'
linear_algebra.matrix.charpoly.linear_map: 'No'
linear_algebra.matrix.charpoly.minpoly: 'No'
linear_algebra.matrix.circulant: 'No'
linear_algebra.matrix.determinant: 'No'
linear_algebra.matrix.diagonal: 'No'
linear_algebra.matrix.dot_product: 'No'
linear_algebra.matrix.dual: 'No'
linear_algebra.matrix.finite_dimensional: 'No'
linear_algebra.matrix.general_linear_group: 'No'
linear_algebra.matrix.hermitian: 'No'
linear_algebra.matrix.invariant_basis_number: 'No'
linear_algebra.matrix.is_diag: 'No'
linear_algebra.matrix.ldl: 'No'
linear_algebra.matrix.mv_polynomial: 'No'
linear_algebra.matrix.nondegenerate: 'No'
linear_algebra.matrix.nonsingular_inverse: 'No'
linear_algebra.matrix.orthogonal: 'No'
linear_algebra.matrix.polynomial: 'No'
linear_algebra.matrix.pos_def: 'No'
linear_algebra.matrix.reindex: 'No'
linear_algebra.matrix.schur_complement: 'No'
linear_algebra.matrix.sesquilinear_form: 'No'
linear_algebra.matrix.special_linear_group: 'No'
linear_algebra.matrix.spectrum: 'No'
linear_algebra.matrix.symmetric: 'No'
linear_algebra.matrix.to_lin: 'No'
linear_algebra.matrix.to_linear_equiv: 'No'
linear_algebra.matrix.trace: 'No'
linear_algebra.matrix.transvection: 'No'
linear_algebra.matrix.zpow: 'No'
linear_algebra.multilinear.basic: No mathlib4#2450 44b58b42794e5abe2bf86397c38e26b587e07e59
linear_algebra.multilinear.basis: 'No'
linear_algebra.multilinear.finite_dimensional: 'No'
linear_algebra.multilinear.tensor_product: 'No'
linear_algebra.orientation: 'No'
linear_algebra.pi: Yes mathlib4#2250 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
linear_algebra.pi_tensor_product: 'No'
linear_algebra.prod: Yes mathlib4#2415 bd9851ca476957ea4549eb19b40e7b5ade9428cc
linear_algebra.projection: Yes mathlib4#2431 6d584f1709bedbed9175bd9350df46599bdd7213
linear_algebra.projective_space.basic: 'No'
linear_algebra.projective_space.independence: 'No'
linear_algebra.projective_space.subspace: 'No'
linear_algebra.quadratic_form.basic: 'No'
linear_algebra.quadratic_form.complex: 'No'
linear_algebra.quadratic_form.isometry: 'No'
linear_algebra.quadratic_form.prod: 'No'
linear_algebra.quadratic_form.real: 'No'
linear_algebra.quotient: Yes mathlib4#2286 48085f140e684306f9e7da907cd5932056d1aded
linear_algebra.quotient_pi: No mathlib4#2378 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
linear_algebra.ray: Yes mathlib4#2468 0f6670b8af2dff699de1c0b4b49039b31bc13c46
linear_algebra.sesquilinear_form: Yes mathlib4#2607 87c54600fe3cdc7d32ff5b50873ac724d86aef8d
linear_algebra.smodeq: Yes mathlib4#2788 146d3d1fa59c091fedaad8a4afa09d6802886d24
linear_algebra.span: Yes mathlib4#2248 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
linear_algebra.std_basis: 'No'
linear_algebra.symplectic_group: 'No'
linear_algebra.tensor_algebra.basic: 'No'
linear_algebra.tensor_algebra.grading: 'No'
linear_algebra.tensor_power: 'No'
linear_algebra.tensor_product: Yes mathlib4#2539 b0c712376e4ef44c53c3b872157ef44dfe9f9599
linear_algebra.tensor_product_basis: 'No'
linear_algebra.trace: 'No'
linear_algebra.unitary_group: 'No'
linear_algebra.vandermonde: 'No'
logic.basic: Yes _ d2d8742b0c21426362a9dacebc6005db895ca963
logic.denumerable: Yes mathlib4#1682 509de852e1de55e1efa8eacfa11df0823f26f226
logic.embedding.basic: Yes mathlib4#700 70d50ecfd4900dd6d328da39ab7ebd516abe4025
logic.embedding.set: Yes mathlib4#986 fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
logic.encodable.basic: Yes mathlib4#1517 7c523cb78f4153682c2929e3006c863bfef463d0
logic.encodable.lattice: Yes mathlib4#1571 9003f28797c0664a49e4179487267c494477d853
logic.equiv.array: No mathlib4#1733 1126441d6bccf98c81214a0780c73d499f6721fe currently
  contains `d_array`s which I believe are not in Lean 4; maybe see `data.array.lemmas`
  above?
logic.equiv.basic: Yes mathlib4#631 d2d8742b0c21426362a9dacebc6005db895ca963
logic.equiv.defs: Yes mathlib4#550 c4658a649d216f57e99621708b09dcb3dcccbd23
logic.equiv.embedding: Yes mathlib4#1021 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
logic.equiv.fin: Yes mathlib4#1745 bd835ef554f37ef9b804f0903089211f89cb370b
logic.equiv.fintype: Yes mathlib4#2524 9407b03373c8cd201df99d6bc5514fc2db44054f
logic.equiv.functor: Yes mathlib4#2577 9407b03373c8cd201df99d6bc5514fc2db44054f
logic.equiv.list: Yes mathlib4#1709 1126441d6bccf98c81214a0780c73d499f6721fe
logic.equiv.local_equiv: Yes mathlib4#331 aba57d4d3dae35460225919dcd82fe91355162f9
logic.equiv.nat: Yes mathlib4#1227 207cfac9fcd06138865b5d04f7091e46d9320432
logic.equiv.option: Yes mathlib4#674 70d50ecfd4900dd6d328da39ab7ebd516abe4025
logic.equiv.set: Yes mathlib4#1044 aba57d4d3dae35460225919dcd82fe91355162f9
logic.equiv.transfer_instance: 'No'
logic.function.basic: Yes mathlib4#13 d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
logic.function.conjugate: Yes mathlib4#533 c4658a649d216f57e99621708b09dcb3dcccbd23
logic.function.iterate: Yes mathlib4#585 792a2a264169d64986541c6f8f7e3bbb6acb6295
logic.hydra: No mathlib4#2290 48085f140e684306f9e7da907cd5932056d1aded
logic.is_empty: Yes mathlib4#486 c4658a649d216f57e99621708b09dcb3dcccbd23
logic.lemmas: Yes mathlib4#537 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
logic.nonempty: Yes mathlib4#160 d2d8742b0c21426362a9dacebc6005db895ca963
logic.nontrivial: Yes mathlib4#520 f340f229b1f461aa1c8ee11e0a172d0a3b301a4a
logic.pairwise: Yes mathlib4#622 c4658a649d216f57e99621708b09dcb3dcccbd23
logic.relation: Yes mathlib4#565 c4658a649d216f57e99621708b09dcb3dcccbd23
logic.relator: Yes mathlib4#385 c4658a649d216f57e99621708b09dcb3dcccbd23
logic.small.basic: Yes mathlib4#1079 d012cd09a9b256d870751284dd6a29882b0be105
logic.small.list: Yes mathlib4#1701 509de852e1de55e1efa8eacfa11df0823f26f226
logic.unique: Yes mathlib4#512 c4658a649d216f57e99621708b09dcb3dcccbd23
measure_theory.card_measurable_space: Yes mathlib4#2516 f2b108e8e97ba393f22bf794989984ddcc1da89b
measure_theory.category.Meas: 'No'
measure_theory.constructions.borel_space: 'No'
measure_theory.constructions.pi: 'No'
measure_theory.constructions.polish: 'No'
measure_theory.constructions.prod: 'No'
measure_theory.covering.besicovitch: 'No'
measure_theory.covering.besicovitch_vector_space: 'No'
measure_theory.covering.density_theorem: 'No'
measure_theory.covering.differentiation: 'No'
measure_theory.covering.liminf_limsup: 'No'
measure_theory.covering.one_dim: 'No'
measure_theory.covering.vitali: 'No'
measure_theory.covering.vitali_family: 'No'
measure_theory.decomposition.jordan: 'No'
measure_theory.decomposition.lebesgue: 'No'
measure_theory.decomposition.radon_nikodym: 'No'
measure_theory.decomposition.signed_hahn: 'No'
measure_theory.decomposition.unsigned_hahn: 'No'
measure_theory.function.ae_eq_fun: 'No'
measure_theory.function.ae_eq_of_integral: 'No'
measure_theory.function.ae_measurable_order: 'No'
measure_theory.function.ae_measurable_sequence: No mathlib4#2358 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
measure_theory.function.conditional_expectation.basic: 'No'
measure_theory.function.conditional_expectation.indicator: 'No'
measure_theory.function.conditional_expectation.real: 'No'
measure_theory.function.continuous_map_dense: 'No'
measure_theory.function.convergence_in_measure: 'No'
measure_theory.function.egorov: 'No'
measure_theory.function.ess_sup: 'No'
measure_theory.function.floor: 'No'
measure_theory.function.jacobian: 'No'
measure_theory.function.l1_space: 'No'
measure_theory.function.l2_space: 'No'
measure_theory.function.locally_integrable: 'No'
measure_theory.function.lp_order: 'No'
measure_theory.function.lp_space: 'No'
measure_theory.function.simple_func_dense: 'No'
measure_theory.function.simple_func_dense_lp: 'No'
measure_theory.function.special_functions.arctan: 'No'
measure_theory.function.special_functions.basic: 'No'
measure_theory.function.special_functions.inner: 'No'
measure_theory.function.strongly_measurable.basic: 'No'
measure_theory.function.strongly_measurable.inner: 'No'
measure_theory.function.strongly_measurable.lp: 'No'
measure_theory.function.uniform_integrable: 'No'
measure_theory.group.action: 'No'
measure_theory.group.add_circle: 'No'
measure_theory.group.arithmetic: 'No'
measure_theory.group.fundamental_domain: 'No'
measure_theory.group.integration: 'No'
measure_theory.group.measurable_equiv: 'No'
measure_theory.group.measure: 'No'
measure_theory.group.pointwise: 'No'
measure_theory.group.prod: 'No'
measure_theory.integral.average: 'No'
measure_theory.integral.bochner: 'No'
measure_theory.integral.circle_integral: 'No'
measure_theory.integral.circle_transform: 'No'
measure_theory.integral.divergence_theorem: 'No'
measure_theory.integral.exp_decay: 'No'
measure_theory.integral.integrable_on: 'No'
measure_theory.integral.integral_eq_improper: 'No'
measure_theory.integral.interval_average: 'No'
measure_theory.integral.interval_integral: 'No'
measure_theory.integral.layercake: 'No'
measure_theory.integral.lebesgue: 'No'
measure_theory.integral.mean_inequalities: 'No'
measure_theory.integral.peak_function: 'No'
measure_theory.integral.periodic: 'No'
measure_theory.integral.riesz_markov_kakutani: 'No'
measure_theory.integral.set_integral: 'No'
measure_theory.integral.set_to_l1: 'No'
measure_theory.integral.torus_integral: 'No'
measure_theory.integral.vitali_caratheodory: 'No'
measure_theory.lattice: 'No'
measure_theory.measurable_space: Yes mathlib4#2174 d101e93197bb5f6ea89bd7ba386b7f7dff1f3903
measure_theory.measurable_space_def: Yes mathlib4#2108 4c19a16e4b705bf135cf9a80ac18fcc99c438514
measure_theory.measure.ae_disjoint: 'No'
measure_theory.measure.ae_measurable: 'No'
measure_theory.measure.complex: 'No'
measure_theory.measure.complex_lebesgue: 'No'
measure_theory.measure.content: 'No'
measure_theory.measure.doubling: 'No'
measure_theory.measure.finite_measure: 'No'
measure_theory.measure.giry_monad: 'No'
measure_theory.measure.haar: 'No'
measure_theory.measure.haar_lebesgue: 'No'
measure_theory.measure.haar_of_basis: 'No'
measure_theory.measure.haar_of_inner: 'No'
measure_theory.measure.haar_quotient: 'No'
measure_theory.measure.hausdorff: 'No'
measure_theory.measure.lebesgue: 'No'
measure_theory.measure.measure_space: 'No'
measure_theory.measure.measure_space_def: 'No'
measure_theory.measure.mutually_singular: 'No'
measure_theory.measure.null_measurable: 'No'
measure_theory.measure.open_pos: 'No'
measure_theory.measure.outer_measure: 'No'
measure_theory.measure.portmanteau: 'No'
measure_theory.measure.probability_measure: 'No'
measure_theory.measure.regular: 'No'
measure_theory.measure.stieltjes: 'No'
measure_theory.measure.sub: 'No'
measure_theory.measure.vector_measure: 'No'
measure_theory.measure.with_density_vector_measure: 'No'
measure_theory.pi_system: Yes mathlib4#2160 98e83c3d541c77cdb7da20d79611a780ff8e7d90
measure_theory.tactic: 'No'
model_theory.basic: No mathlib4#2296 369525b73f229ccd76a6ec0e0e0bf2be57599768
model_theory.bundled: 'No'
model_theory.definability: 'No'
model_theory.direct_limit: 'No'
model_theory.elementary_maps: 'No'
model_theory.encoding: 'No'
model_theory.finitely_generated: 'No'
model_theory.fraisse: 'No'
model_theory.graph: 'No'
model_theory.language_map: 'No'
model_theory.order: 'No'
model_theory.quotients: 'No'
model_theory.satisfiability: 'No'
model_theory.semantics: 'No'
model_theory.skolem: 'No'
model_theory.substructures: 'No'
model_theory.syntax: 'No'
model_theory.types: 'No'
model_theory.ultraproducts: 'No'
number_theory.ADE_inequality: Yes mathlib4#2155 0a0ec35061ed9960bf0e7ffb0335f44447b58977
number_theory.arithmetic_function: 'No'
number_theory.basic: Yes mathlib4#2773 168ad7fc5d8173ad38be9767a22d50b8ecf1cd00
number_theory.bernoulli: 'No'
number_theory.bernoulli_polynomials: 'No'
number_theory.bertrand: 'No'
number_theory.class_number.admissible_abs: Yes mathlib4#2372 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
number_theory.class_number.admissible_absolute_value: Yes mathlib4#1941 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
number_theory.class_number.admissible_card_pow_degree: 'No'
number_theory.class_number.finite: 'No'
number_theory.class_number.function_field: 'No'
number_theory.cyclotomic.basic: 'No'
number_theory.cyclotomic.discriminant: 'No'
number_theory.cyclotomic.gal: 'No'
number_theory.cyclotomic.primitive_roots: 'No'
number_theory.cyclotomic.rat: 'No'
number_theory.dioph: 'No'
number_theory.diophantine_approximation: 'No'
number_theory.divisors: Yes mathlib4#1912 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
number_theory.fermat4: 'No'
number_theory.fermat_psp: 'No'
number_theory.frobenius_number: Yes mathlib4#1719 1126441d6bccf98c81214a0780c73d499f6721fe
number_theory.function_field: 'No'
number_theory.kummer_dedekind: 'No'
number_theory.l_series: 'No'
number_theory.legendre_symbol.add_character: 'No'
number_theory.legendre_symbol.gauss_eisenstein_lemmas: 'No'
number_theory.legendre_symbol.gauss_sum: 'No'
number_theory.legendre_symbol.jacobi_symbol: 'No'
number_theory.legendre_symbol.mul_character: No mathlib4#2994 6623e6af705e97002a9054c1c05a980180276fc1
number_theory.legendre_symbol.norm_num: 'No'
number_theory.legendre_symbol.quadratic_char: 'No'
number_theory.legendre_symbol.quadratic_reciprocity: 'No'
number_theory.legendre_symbol.zmod_char: 'No'
number_theory.liouville.basic: 'No'
number_theory.liouville.liouville_constant: 'No'
number_theory.liouville.liouville_with: 'No'
number_theory.liouville.measure: 'No'
number_theory.liouville.residual: 'No'
number_theory.lucas_lehmer: No mathlib4#2988 10b4e499f43088dd3bb7b5796184ad5216648ab1
number_theory.lucas_primality: 'No'
number_theory.modular: 'No'
number_theory.modular_forms.basic: 'No'
number_theory.modular_forms.congruence_subgroups: 'No'
number_theory.modular_forms.jacobi_theta: 'No'
number_theory.modular_forms.slash_actions: 'No'
number_theory.modular_forms.slash_invariant_forms: 'No'
number_theory.multiplicity: 'No'
number_theory.number_field.basic: 'No'
number_theory.number_field.class_number: 'No'
number_theory.number_field.embeddings: 'No'
number_theory.number_field.norm: 'No'
number_theory.padics.hensel: 'No'
number_theory.padics.padic_integers: 'No'
number_theory.padics.padic_norm: 'No'
number_theory.padics.padic_numbers: 'No'
number_theory.padics.padic_val: Yes mathlib4#3020 60fa54e778c9e85d930efae172435f42fb0d71f7
number_theory.padics.ring_homs: 'No'
number_theory.pell: 'No'
number_theory.pell_matiyasevic: 'No'
number_theory.prime_counting: 'No'
number_theory.primes_congruent_one: 'No'
number_theory.primorial: Yes mathlib4#2137 0a0ec35061ed9960bf0e7ffb0335f44447b58977
number_theory.pythagorean_triples: Yes mathlib4#3022 70fd9563a21e7b963887c9360bd29b2393e6225a
number_theory.ramification_inertia: 'No'
number_theory.sum_four_squares: 'No'
number_theory.sum_two_squares: 'No'
number_theory.von_mangoldt: 'No'
number_theory.well_approximable: 'No'
number_theory.wilson: 'No'
number_theory.zeta_values: 'No'
number_theory.zsqrtd.basic: Yes mathlib4#3034 7ec294687917cbc5c73620b4414ae9b5dd9ae1b4
number_theory.zsqrtd.gaussian_int: 'No'
number_theory.zsqrtd.to_real: Yes mathlib4#3053 e59154361202a34b26176e0de9267ef8e2dcd446
order.antichain: Yes mathlib4#1206 207cfac9fcd06138865b5d04f7091e46d9320432
order.antisymmetrization: Yes mathlib4#876 f1a2caaf51ef593799107fe9a8d5e411599f3996
order.atoms: Yes mathlib4#1257 422e70f7ce183d2900c586a8cda8381e788a0c62
order.atoms.finite: Yes mathlib4#1756 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
order.basic: Yes mathlib4#348 1f0096e6caa61e9c849ec2adbd227e960e9dff58
order.boolean_algebra: Yes mathlib4#794 bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e
order.bounded: Yes mathlib4#1042 aba57d4d3dae35460225919dcd82fe91355162f9
order.bounded_order: Yes mathlib4#697 70d50ecfd4900dd6d328da39ab7ebd516abe4025
order.bounds.basic: Yes mathlib4#1040 3310acfa9787aa171db6d4cba3945f6f275fe9f2
order.bounds.order_iso: Yes mathlib4#1063 a59dad53320b73ef180174aae867addd707ef00e
order.category.BoolAlg: 'No'
order.category.BoundedDistribLattice: 'No'
order.category.BoundedLattice: 'No'
order.category.BoundedOrder: 'No'
order.category.CompleteLattice: 'No'
order.category.DistribLattice: 'No'
order.category.FinBoolAlg: 'No'
order.category.FinPartialOrder: 'No'
order.category.Frame: 'No'
order.category.HeytAlg: 'No'
order.category.Lattice: 'No'
order.category.LinearOrder: 'No'
order.category.NonemptyFinLinOrd: 'No'
order.category.PartialOrder: 'No'
order.category.Preorder: 'No'
order.category.Semilattice: 'No'
order.category.omega_complete_partial_order: 'No'
order.chain: Yes mathlib4#1205 207cfac9fcd06138865b5d04f7091e46d9320432
order.circular: Yes mathlib4#1489 a2d2e18906e2b62627646b5d5be856e6a642062f waiting
  on tauto; WIP @thorimur
order.closure: Yes mathlib4#1263 f252872231e87a5db80d9938fc05530e70f23a94
order.compactly_generated: Yes mathlib4#1976 861a26926586cd46ff80264d121cdb6fa0e35cc1
  needs TFAE tactic
order.compare: Yes mathlib4#569 c4658a649d216f57e99621708b09dcb3dcccbd23
order.complete_boolean_algebra: Yes mathlib4#1107 c5c7e2760814660967bc27f0de95d190a22297f3
order.complete_lattice: Yes mathlib4#1053 5709b0d8725255e76f47debca6400c07b5c2d8e6
order.complete_lattice_intervals: Yes mathlib4#1242 207cfac9fcd06138865b5d04f7091e46d9320432
order.concept: Yes mathlib4#1355 1e05171a5e8cf18d98d9cf7b207540acb044acae
order.conditionally_complete_lattice.basic: Yes _ 207cfac9fcd06138865b5d04f7091e46d9320432
order.conditionally_complete_lattice.finset: Yes mathlib4#1748 2445c98ae4b87eabebdde552593519b9b6dc350c
order.conditionally_complete_lattice.group: Yes mathlib4#1253 46a64b5b4268c594af770c44d9e502afc6a515cb
order.copy: Yes mathlib4#1202 207cfac9fcd06138865b5d04f7091e46d9320432
order.countable_dense_linear_order: Yes mathlib4#2037 2705404e701abc6b3127da906f40bae062a169c9
order.cover: Yes mathlib4#1200 207cfac9fcd06138865b5d04f7091e46d9320432
order.directed: Yes mathlib4#963 18a5306c091183ac90884daa9373fa3b178e8607
order.disjoint: Yes mathlib4#773 70d50ecfd4900dd6d328da39ab7ebd516abe4025
order.disjointed: Yes mathlib4#1920 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
order.extension.linear: Yes mathlib4#1309 9830a300340708eaa85d477c3fb96dd25f9468a5
order.extension.well: Yes mathlib4#2333 740acc0e6f9adf4423f92a485d0456fc271482da
order.filter.archimedean: Yes mathlib4#1818 8631e2d5ea77f6c13054d9151d82b83069680cb1
order.filter.at_top_bot: Yes mathlib4#1795 1f0096e6caa61e9c849ec2adbd227e960e9dff58
order.filter.bases: Yes mathlib4#1791 996b0ff959da753a555053a480f36e5f264d4207
order.filter.basic: Yes mathlib4#1750 e1a7bdeb4fd826b7e71d130d34988f0a2d26a177
order.filter.cofinite: Yes mathlib4#1813 8631e2d5ea77f6c13054d9151d82b83069680cb1
order.filter.countable_Inter: Yes mathlib4#1803 8631e2d5ea77f6c13054d9151d82b83069680cb1
order.filter.curry: Yes mathlib4#1773 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
order.filter.ennreal: Yes mathlib4#2512 11c2b8c18d1a8e44fe9ba8ba6b931d51b4734150
order.filter.extr: Yes mathlib4#1785 1f0096e6caa61e9c849ec2adbd227e960e9dff58
order.filter.filter_product: Yes mathlib4#2366 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
order.filter.germ: Yes mathlib4#1799 1f0096e6caa61e9c849ec2adbd227e960e9dff58
order.filter.indicator_function: Yes mathlib4#1821 8631e2d5ea77f6c13054d9151d82b83069680cb1
order.filter.interval: Yes mathlib4#1820 8631e2d5ea77f6c13054d9151d82b83069680cb1
order.filter.lift: Yes mathlib4#1804 8631e2d5ea77f6c13054d9151d82b83069680cb1
order.filter.modeq: Yes mathlib4#1929 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
order.filter.n_ary: Yes mathlib4#1786 1f0096e6caa61e9c849ec2adbd227e960e9dff58
order.filter.partial: Yes mathlib4#2059 b363547b3113d350d053abdf2884e9850a56b205
order.filter.pi: Yes mathlib4#1802 1f0096e6caa61e9c849ec2adbd227e960e9dff58
order.filter.pointwise: Yes mathlib4#1839 e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
order.filter.prod: Yes mathlib4#1772 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
order.filter.small_sets: Yes mathlib4#1810 8631e2d5ea77f6c13054d9151d82b83069680cb1
order.filter.ultrafilter: Yes mathlib4#1814 8631e2d5ea77f6c13054d9151d82b83069680cb1
order.filter.zero_and_bounded_at_filter: 'No'
order.fixed_points: Yes mathlib4#1174 ba2245edf0c8bb155f1569fd9b9492a9b384cde6
order.galois_connection: Yes mathlib4#1099 c5c7e2760814660967bc27f0de95d190a22297f3
order.game_add: Yes mathlib4#645 99e8971dc62f1f7ecf693d75e75fbbabd55849de
order.grade: Yes mathlib4#1594 9003f28797c0664a49e4179487267c494477d853
order.height: No mathlib4#2186 dde670c9a3f503647fd5bfdf1037bad526d3397a
order.heyting.basic: Yes mathlib4#793 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e
order.heyting.boundary: Yes mathlib4#844 70d50ecfd4900dd6d328da39ab7ebd516abe4025
order.heyting.hom: Yes mathlib4#2077 4c19a16e4b705bf135cf9a80ac18fcc99c438514
order.heyting.regular: Yes mathlib4#1269 09597669f02422ed388036273d8848119699c22f
order.hom.basic: Yes mathlib4#804 62a5626868683c104774de8d85b9855234ac807c
order.hom.bounded: Yes mathlib4#888 f1a2caaf51ef593799107fe9a8d5e411599f3996 Blocked
  by type class issue. Impossible to satisfy the linter
order.hom.complete_lattice: Yes mathlib4#2054 bcfa726826abd57587355b4b5b7e78ad6527b7e4
order.hom.lattice: Yes mathlib4#1636 9003f28797c0664a49e4179487267c494477d853
order.hom.order: Yes mathlib4#1152 ba2245edf0c8bb155f1569fd9b9492a9b384cde6
order.hom.set: Yes mathlib4#1059 198161d833f2c01498c39c266b0b3dbe2c7a8c07
order.ideal: Yes mathlib4#1985 59694bd07f0a39c5beccba34bd9f413a160782bf
order.initial_seg: Yes mathlib4#1012 8da9e30545433fdd8fe55a0d3da208e5d9263f03
order.interval: No mathlib4#1272 09597669f02422ed388036273d8848119699c22f
order.iterate: Yes mathlib4#648 2258b40dacd2942571c8ce136215350c702dc78f
order.jordan_holder: Yes mathlib4#2578 91288e351d51b3f0748f0a38faa7613fb0ae2ada
order.lattice: Yes mathlib4#642 d6aad9528ddcac270ed35c6f7b5f1d8af25341d6
order.lattice_intervals: Yes mathlib4#1070 d012cd09a9b256d870751284dd6a29882b0be105
order.liminf_limsup: Yes mathlib4#2078 4c19a16e4b705bf135cf9a80ac18fcc99c438514
order.locally_finite: Yes mathlib4#1754 2445c98ae4b87eabebdde552593519b9b6dc350c
order.max: Yes mathlib4#567 6623e6af705e97002a9054c1c05a980180276fc1
order.min_max: Yes mathlib4#728 70d50ecfd4900dd6d328da39ab7ebd516abe4025
order.minimal: Yes mathlib4#1914 59694bd07f0a39c5beccba34bd9f413a160782bf
order.modular_lattice: Yes mathlib4#1234 207cfac9fcd06138865b5d04f7091e46d9320432
order.monotone.basic: Yes mathlib4#947 ac5a7cec422c3909db52e13dde2e729657d19b0e
order.monotone.extension: Yes mathlib4#1262 422e70f7ce183d2900c586a8cda8381e788a0c62
order.monotone.monovary: Yes mathlib4#1085 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
order.monotone.odd: Yes mathlib4#1162 9116dd6709f303dcf781632e15fdef382b0fc579
order.monotone.union: Yes mathlib4#1083 d012cd09a9b256d870751284dd6a29882b0be105
order.omega_complete_partial_order: Yes mathlib4#1168 92ca63f0fb391a9ca5f22d2409a6080e786d99f7
order.ord_continuous: Yes mathlib4#1241 207cfac9fcd06138865b5d04f7091e46d9320432
order.order_iso_nat: Yes mathlib4#1753 6623e6af705e97002a9054c1c05a980180276fc1
order.partial_sups: Yes mathlib4#1757 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
order.partition.equipartition: Yes mathlib4#2058 b363547b3113d350d053abdf2884e9850a56b205
order.partition.finpartition: Yes mathlib4#1765 d6fad0e5bf2d6f48da9175d25c3dc5706b3834ce
order.pfilter: Yes mathlib4#2351 740acc0e6f9adf4423f92a485d0456fc271482da
order.prime_ideal: Yes mathlib4#2352 740acc0e6f9adf4423f92a485d0456fc271482da
order.prop_instances: Yes mathlib4#792 6623e6af705e97002a9054c1c05a980180276fc1
order.rel_classes: Yes mathlib4#560 bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e
order.rel_iso.basic: Yes mathlib4#772 76171581280d5b5d1e2d1f4f37e5420357bdc636
order.rel_iso.group: Yes mathlib4#813 62a5626868683c104774de8d85b9855234ac807c
order.rel_iso.set: Yes mathlib4#1005 ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
order.semiconj_Sup: Yes mathlib4#1265 422e70f7ce183d2900c586a8cda8381e788a0c62
order.succ_pred.basic: Yes mathlib4#1233 0111834459f5d7400215223ea95ae38a1265a907
order.succ_pred.interval_succ: Yes mathlib4#1301 1e05171a5e8cf18d98d9cf7b207540acb044acae
order.succ_pred.limit: Yes mathlib4#1300 1e05171a5e8cf18d98d9cf7b207540acb044acae
order.succ_pred.linear_locally_finite: Yes mathlib4#2033 2705404e701abc6b3127da906f40bae062a169c9
order.succ_pred.relation: Yes mathlib4#1295 9aba7801eeecebb61f58a5763c2b6dd1b47dc6ef
order.sup_indep: Yes mathlib4#1627 1c857a1f6798cb054be942199463c2cf904cb937
order.symm_diff: Yes mathlib4#842 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904
order.synonym: Yes mathlib4#562 c4658a649d216f57e99621708b09dcb3dcccbd23
order.upper_lower.basic: Yes mathlib4#1978 59694bd07f0a39c5beccba34bd9f413a160782bf
order.upper_lower.hom: Yes mathlib4#2154 0a0ec35061ed9960bf0e7ffb0335f44447b58977
order.well_founded: Yes mathlib4#970 1c521b4fb909320eca16b2bb6f8b5b0490b1cb5e
order.well_founded_set: Yes mathlib4#1975 bcfa726826abd57587355b4b5b7e78ad6527b7e4
order.with_bot: Yes mathlib4#777 0111834459f5d7400215223ea95ae38a1265a907
order.zorn: Yes mathlib4#1254 46a64b5b4268c594af770c44d9e502afc6a515cb
order.zorn_atoms: Yes mathlib4#1293 9aba7801eeecebb61f58a5763c2b6dd1b47dc6ef
probability.borel_cantelli: 'No'
probability.cond_count: 'No'
probability.conditional_expectation: 'No'
probability.conditional_probability: 'No'
probability.density: 'No'
probability.ident_distrib: 'No'
probability.independence: 'No'
probability.integration: 'No'
probability.kernel.basic: 'No'
probability.kernel.composition: 'No'
probability.kernel.invariance: 'No'
probability.martingale.basic: 'No'
probability.martingale.borel_cantelli: 'No'
probability.martingale.centering: 'No'
probability.martingale.convergence: 'No'
probability.martingale.optional_stopping: 'No'
probability.martingale.upcrossing: 'No'
probability.moments: 'No'
probability.notation: 'No'
probability.probability_mass_function.basic: 'No'
probability.probability_mass_function.constructions: 'No'
probability.probability_mass_function.monad: 'No'
probability.probability_mass_function.uniform: 'No'
probability.process.adapted: 'No'
probability.process.filtration: 'No'
probability.process.hitting_time: 'No'
probability.process.stopping: 'No'
probability.strong_law: 'No'
probability.variance: 'No'
representation_theory.Action: 'No'
representation_theory.Rep: 'No'
representation_theory.basic: 'No'
representation_theory.character: 'No'
representation_theory.fdRep: 'No'
representation_theory.group_cohomology_resolution: 'No'
representation_theory.invariants: 'No'
representation_theory.maschke: No mathlib4#2986 70fd9563a21e7b963887c9360bd29b2393e6225a
ring_theory.adjoin.basic: Yes mathlib4#2817 a35ddf20601f85f78cd57e7f5b09ed528d71b7af
ring_theory.adjoin.fg: 'No'
ring_theory.adjoin.field: 'No'
ring_theory.adjoin.power_basis: 'No'
ring_theory.adjoin.tower: 'No'
ring_theory.adjoin_root: 'No'
ring_theory.algebra_tower: Yes mathlib4#2586 94825b2b0b982306be14d891c4f063a1eca4f370
ring_theory.algebraic: 'No'
ring_theory.algebraic_independent: 'No'
ring_theory.artinian: 'No'
ring_theory.bezout: 'No'
ring_theory.chain_of_divisors: No mathlib4#3056 f694c7dead66f5d4c80f446c796a5aad14707f0e
ring_theory.class_group: 'No'
ring_theory.congruence: Yes mathlib4#1629 9003f28797c0664a49e4179487267c494477d853
ring_theory.coprime.basic: Yes mathlib4#899 a95b16cbade0f938fc24abd05412bde1e84bab9b
ring_theory.coprime.ideal: Yes mathlib4#2903 2bbc7e3884ba234309d2a43b19144105a753292e
ring_theory.coprime.lemmas: Yes mathlib4#1692 509de852e1de55e1efa8eacfa11df0823f26f226
ring_theory.dedekind_domain.S_integer: 'No'
ring_theory.dedekind_domain.adic_valuation: 'No'
ring_theory.dedekind_domain.basic: 'No'
ring_theory.dedekind_domain.dvr: 'No'
ring_theory.dedekind_domain.factorization: 'No'
ring_theory.dedekind_domain.finite_adele_ring: 'No'
ring_theory.dedekind_domain.ideal: 'No'
ring_theory.dedekind_domain.integral_closure: 'No'
ring_theory.dedekind_domain.pid: 'No'
ring_theory.dedekind_domain.selmer_group: 'No'
ring_theory.derivation: 'No'
ring_theory.discrete_valuation_ring: 'No'
ring_theory.discriminant: 'No'
ring_theory.eisenstein_criterion: 'No'
ring_theory.etale: 'No'
ring_theory.euclidean_domain: Yes mathlib4#3017 70fd9563a21e7b963887c9360bd29b2393e6225a
ring_theory.filtration: 'No'
ring_theory.finite_presentation: 'No'
ring_theory.finite_type: 'No'
ring_theory.finiteness: Yes mathlib4#2811 f5edf4694f7c478cbca7a2451bddbd221fc7f869
ring_theory.fintype: Yes mathlib4#1712 1126441d6bccf98c81214a0780c73d499f6721fe
ring_theory.flat: Yes mathlib4#3009 62c0a4ef1441edb463095ea02a06e87f3dfe135c
ring_theory.fractional_ideal: 'No'
ring_theory.free_comm_ring: 'No'
ring_theory.free_ring: Yes mathlib4#2885 d6814c584384ddf2825ff038e868451a7c956f31
ring_theory.graded_algebra.basic: 'No'
ring_theory.graded_algebra.homogeneous_ideal: 'No'
ring_theory.graded_algebra.homogeneous_localization: 'No'
ring_theory.graded_algebra.radical: 'No'
ring_theory.hahn_series: 'No'
ring_theory.henselian: 'No'
ring_theory.ideal.associated_prime: 'No'
ring_theory.ideal.basic: Yes mathlib4#2283 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
ring_theory.ideal.cotangent: 'No'
ring_theory.ideal.idempotent_fg: Yes mathlib4#2980 25cf7631da8ddc2d5f957c388bf5e4b25a77d8dc
ring_theory.ideal.local_ring: 'No'
ring_theory.ideal.minimal_prime: 'No'
ring_theory.ideal.norm: 'No'
ring_theory.ideal.operations: Yes mathlib4#2701 e7f0ddbf65bd7181a85edb74b64bdc35ba4bdc74
ring_theory.ideal.over: 'No'
ring_theory.ideal.prod: Yes mathlib4#2877 052f6013363326d50cb99c6939814a4b8eb7b301
ring_theory.ideal.quotient: Yes mathlib4#2412 bd9851ca476957ea4549eb19b40e7b5ade9428cc
ring_theory.ideal.quotient_operations: No mathlib4#2757 e7f0ddbf65bd7181a85edb74b64bdc35ba4bdc74
ring_theory.int.basic: Yes mathlib4#3014 2196ab363eb097c008d4497125e0dde23fb36db2
ring_theory.integral_closure: 'No'
ring_theory.integral_domain: 'No'
ring_theory.integrally_closed: 'No'
ring_theory.is_adjoin_root: 'No'
ring_theory.is_tensor_product: 'No'
ring_theory.jacobson: 'No'
ring_theory.jacobson_ideal: 'No'
ring_theory.laurent_series: 'No'
ring_theory.local_properties: 'No'
ring_theory.localization.as_subring: 'No'
ring_theory.localization.at_prime: 'No'
ring_theory.localization.away: 'No'
ring_theory.localization.basic: Yes mathlib4#2741 b69c9a770ecf37eb21f7b8cf4fa00de3b62694ec
ring_theory.localization.cardinality: 'No'
ring_theory.localization.fraction_ring: Yes mathlib4#2763 831c494092374cfe9f50591ed0ac81a25efc5b86
ring_theory.localization.ideal: 'No'
ring_theory.localization.integer: Yes mathlib4#2875 9556784a5b84697562e9c6acb40500d4a82e675a
ring_theory.localization.integral: 'No'
ring_theory.localization.inv_submonoid: 'No'
ring_theory.localization.localization_localization: 'No'
ring_theory.localization.module: 'No'
ring_theory.localization.norm: 'No'
ring_theory.localization.num_denom: Yes mathlib4#3044 831c494092374cfe9f50591ed0ac81a25efc5b86
ring_theory.localization.submodule: 'No'
ring_theory.matrix_algebra: 'No'
ring_theory.multiplicity: Yes mathlib4#2962 ceb887ddf3344dab425292e497fa2af91498437c
ring_theory.mv_polynomial.basic: 'No'
ring_theory.mv_polynomial.homogeneous: 'No'
ring_theory.mv_polynomial.symmetric: Yes mathlib4#2981 70fd9563a21e7b963887c9360bd29b2393e6225a
ring_theory.mv_polynomial.tower: Yes mathlib4#2897 bb168510ef455e9280a152e7f31673cabd3d7496
ring_theory.nakayama: 'No'
ring_theory.nilpotent: Yes mathlib4#2829 da420a8c6dd5bdfb85c4ced85c34388f633bc6ff
ring_theory.noetherian: Yes mathlib4#2976 da420a8c6dd5bdfb85c4ced85c34388f633bc6ff
ring_theory.non_unital_subsemiring.basic: No mathlib4#1774 1f0096e6caa61e9c849ec2adbd227e960e9dff58
ring_theory.non_zero_divisors: Yes mathlib4#1717 1126441d6bccf98c81214a0780c73d499f6721fe
ring_theory.norm: 'No'
ring_theory.nullstellensatz: 'No'
ring_theory.ore_localization.basic: Yes mathlib4#1964 861a26926586cd46ff80264d121cdb6fa0e35cc1
ring_theory.ore_localization.ore_set: Yes mathlib4#1266 422e70f7ce183d2900c586a8cda8381e788a0c62
ring_theory.perfection: 'No'
ring_theory.polynomial.basic: 'No'
ring_theory.polynomial.bernstein: 'No'
ring_theory.polynomial.chebyshev: Yes mathlib4#2880 d774451114d6045faeb6751c396bea1eb9058946
ring_theory.polynomial.content: 'No'
ring_theory.polynomial.cyclotomic.basic: 'No'
ring_theory.polynomial.cyclotomic.eval: 'No'
ring_theory.polynomial.dickson: 'No'
ring_theory.polynomial.eisenstein.basic: 'No'
ring_theory.polynomial.eisenstein.is_integral: 'No'
ring_theory.polynomial.gauss_lemma: 'No'
ring_theory.polynomial.opposites: Yes mathlib4#2868 63417e01fbc711beaf25fa73b6edb395c0cfddd0
ring_theory.polynomial.pochhammer: Yes mathlib4#2733 53b216bcc1146df1c4a0a86877890ea9f1f01589
ring_theory.polynomial.quotient: 'No'
ring_theory.polynomial.rational_root: 'No'
ring_theory.polynomial.scale_roots: Yes mathlib4#2841 40ac1b258344e0c2b4568dc37bfad937ec35a727
ring_theory.polynomial.selmer: 'No'
ring_theory.polynomial.tower: Yes mathlib4#2840 bb168510ef455e9280a152e7f31673cabd3d7496
ring_theory.polynomial.vieta: 'No'
ring_theory.polynomial_algebra: 'No'
ring_theory.power_basis: 'No'
ring_theory.power_series.basic: 'No'
ring_theory.power_series.well_known: 'No'
ring_theory.prime: Yes mathlib4#1646 008205aa645b3f194c1da47025c5f110c8406eab
ring_theory.principal_ideal_domain: Yes mathlib4#3012 6010cf523816335f7bae7f8584cb2edaace73940
ring_theory.quotient_nilpotent: 'No'
ring_theory.quotient_noetherian: 'No'
ring_theory.rees_algebra: 'No'
ring_theory.ring_hom.finite: 'No'
ring_theory.ring_hom.finite_type: 'No'
ring_theory.ring_hom.integral: 'No'
ring_theory.ring_hom.surjective: 'No'
ring_theory.ring_hom_properties: 'No'
ring_theory.ring_invo: Yes mathlib4#1276 09597669f02422ed388036273d8848119699c22f
ring_theory.roots_of_unity: 'No'
ring_theory.simple_module: 'No'
ring_theory.subring.basic: Yes mathlib4#1945 feb99064803fd3108e37c18b0f77d0a8344677a3
ring_theory.subring.pointwise: Yes mathlib4#2212 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
ring_theory.subsemiring.basic: Yes mathlib4#1862 feb99064803fd3108e37c18b0f77d0a8344677a3
ring_theory.subsemiring.pointwise: Yes mathlib4#1983 59694bd07f0a39c5beccba34bd9f413a160782bf
ring_theory.tensor_product: 'No'
ring_theory.trace: 'No'
ring_theory.unique_factorization_domain: Yes mathlib4#3003 f694c7dead66f5d4c80f446c796a5aad14707f0e
ring_theory.valuation.basic: Yes mathlib4#2846 da420a8c6dd5bdfb85c4ced85c34388f633bc6ff
ring_theory.valuation.extend_to_localization: 'No'
ring_theory.valuation.integers: Yes mathlib4#2966 7b7da89322fe46a16bf03eeb345b0acfc73fe10e
ring_theory.valuation.integral: 'No'
ring_theory.valuation.quotient: 'No'
ring_theory.valuation.ramification_group: 'No'
ring_theory.valuation.tfae: 'No'
ring_theory.valuation.valuation_ring: 'No'
ring_theory.valuation.valuation_subring: 'No'
ring_theory.witt_vector.basic: 'No'
ring_theory.witt_vector.compare: 'No'
ring_theory.witt_vector.defs: 'No'
ring_theory.witt_vector.discrete_valuation_ring: 'No'
ring_theory.witt_vector.domain: 'No'
ring_theory.witt_vector.frobenius: 'No'
ring_theory.witt_vector.frobenius_fraction_field: 'No'
ring_theory.witt_vector.identities: 'No'
ring_theory.witt_vector.init_tail: 'No'
ring_theory.witt_vector.is_poly: 'No'
ring_theory.witt_vector.isocrystal: 'No'
ring_theory.witt_vector.mul_coeff: 'No'
ring_theory.witt_vector.mul_p: 'No'
ring_theory.witt_vector.structure_polynomial: 'No'
ring_theory.witt_vector.teichmuller: 'No'
ring_theory.witt_vector.truncated: 'No'
ring_theory.witt_vector.verschiebung: 'No'
ring_theory.witt_vector.witt_polynomial: 'No'
set_theory.cardinal.basic: Yes mathlib4#2084 4c19a16e4b705bf135cf9a80ac18fcc99c438514
set_theory.cardinal.cofinality: Yes mathlib4#2479 bb168510ef455e9280a152e7f31673cabd3d7496
set_theory.cardinal.continuum: Yes mathlib4#2474 3d7987cda72abc473c7cdbbb075170e9ac620042
set_theory.cardinal.divisibility: Yes mathlib4#2473 92ca63f0fb391a9ca5f22d2409a6080e786d99f7
set_theory.cardinal.finite: Yes mathlib4#2182 dde670c9a3f503647fd5bfdf1037bad526d3397a
set_theory.cardinal.ordinal: Yes mathlib4#2463 8da9e30545433fdd8fe55a0d3da208e5d9263f03
set_theory.cardinal.schroeder_bernstein: Yes mathlib4#1296 1e05171a5e8cf18d98d9cf7b207540acb044acae
set_theory.game.basic: 'No'
set_theory.game.birthday: 'No'
set_theory.game.domineering: 'No'
set_theory.game.impartial: 'No'
set_theory.game.nim: 'No'
set_theory.game.ordinal: 'No'
set_theory.game.pgame: No mathlib4#1512 7c523cb78f4153682c2929e3006c863bfef463d0 Contains
  a local tactic `pgame_wf_tac`
set_theory.game.short: 'No'
set_theory.game.state: 'No'
set_theory.lists: Yes mathlib4#1575 497d1e06409995dd8ec95301fa8d8f3480187f4c
set_theory.ordinal.arithmetic: Yes mathlib4#2271 8da9e30545433fdd8fe55a0d3da208e5d9263f03
set_theory.ordinal.basic: Yes mathlib4#2217 8da9e30545433fdd8fe55a0d3da208e5d9263f03
set_theory.ordinal.cantor_normal_form: Yes mathlib4#2471 f1e061e3caef3022f0daa99d670ecf2c30e0b5c6
set_theory.ordinal.exponential: Yes mathlib4#2330 8ee653c07a9ddb27ae466d045a3f0c2151b076cf
set_theory.ordinal.fixed_point: Yes mathlib4#2416 bd9851ca476957ea4549eb19b40e7b5ade9428cc
set_theory.ordinal.natural_ops: Yes mathlib4#2353 740acc0e6f9adf4423f92a485d0456fc271482da
set_theory.ordinal.notation: No mathlib4#2470 9b2660e1b25419042c8da10bf411aa3c67f14383
set_theory.ordinal.principal: Yes mathlib4#2442 9b2660e1b25419042c8da10bf411aa3c67f14383
set_theory.ordinal.topology: Yes mathlib4#2342 740acc0e6f9adf4423f92a485d0456fc271482da
set_theory.surreal.basic: 'No'
set_theory.surreal.dyadic: 'No'
set_theory.zfc.basic: No mathlib4#1215 207cfac9fcd06138865b5d04f7091e46d9320432
set_theory.zfc.ordinal: 'No'
testing.slim_check.functions: 'No'
testing.slim_check.gen: 'No'
testing.slim_check.sampleable: 'No'
testing.slim_check.testable: 'No'
topology.G_delta: Yes mathlib4#2064 b363547b3113d350d053abdf2884e9850a56b205
topology.alexandroff: Yes mathlib4#2229 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.algebra.affine: Yes mathlib4#2693 717c073262cd9d59b1a1dcda7e8ab570c5b63370
topology.algebra.algebra: 'No'
topology.algebra.const_mul_action: Yes mathlib4#2012 d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
topology.algebra.constructions: Yes mathlib4#2011 c10e724be91096453ee3db13862b9fb9a992fef2
topology.algebra.continuous_affine_map: 'No'
topology.algebra.continuous_monoid_hom: 'No'
topology.algebra.equicontinuity: 'No'
topology.algebra.field: Yes mathlib4#2617 c10e724be91096453ee3db13862b9fb9a992fef2
topology.algebra.filter_basis: 'No'
topology.algebra.group.basic: Yes mathlib4#2267 c10e724be91096453ee3db13862b9fb9a992fef2
topology.algebra.group.compact: Yes mathlib4#2420 f2ce6086713c78a7f880485f7917ea547a215982
topology.algebra.group_completion: Yes mathlib4#2637 a148d797a1094ab554ad4183a4ad6f130358ef64
topology.algebra.group_with_zero: Yes mathlib4#2288 c10e724be91096453ee3db13862b9fb9a992fef2
topology.algebra.infinite_sum.basic: Yes mathlib4#2500 32253a1a1071173b33dc7d6a218cf722c6feb514
topology.algebra.infinite_sum.module: 'No'
topology.algebra.infinite_sum.order: Yes mathlib4#2644 32253a1a1071173b33dc7d6a218cf722c6feb514
topology.algebra.infinite_sum.real: Yes mathlib4#2673 9a59dcb7a2d06bf55da57b9030169219980660cd
topology.algebra.infinite_sum.ring: Yes mathlib4#2640 9a59dcb7a2d06bf55da57b9030169219980660cd
topology.algebra.localization: Yes mathlib4#2802 9a59dcb7a2d06bf55da57b9030169219980660cd
topology.algebra.module.basic: No mathlib4#2983 f430769b562e0cedef59ee1ed968d67e0e0c86ba
topology.algebra.module.character_space: 'No'
topology.algebra.module.determinant: 'No'
topology.algebra.module.finite_dimension: 'No'
topology.algebra.module.linear_pmap: 'No'
topology.algebra.module.locally_convex: 'No'
topology.algebra.module.multilinear: 'No'
topology.algebra.module.simple: 'No'
topology.algebra.module.strong_topology: 'No'
topology.algebra.module.weak_dual: 'No'
topology.algebra.monoid: Yes mathlib4#2245 6efec6bb9fcaed3cf1baaddb2eaadd8a2a06679c
topology.algebra.mul_action: Yes mathlib4#2013 d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
topology.algebra.nonarchimedean.adic_topology: 'No'
topology.algebra.nonarchimedean.bases: 'No'
topology.algebra.nonarchimedean.basic: Yes mathlib4#2958 83f81aea33931a1edb94ce0f32b9a5d484de6978
topology.algebra.open_subgroup: Yes mathlib4#2889 83f81aea33931a1edb94ce0f32b9a5d484de6978
topology.algebra.order.archimedean: Yes mathlib4#2083 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.algebra.order.compact: Yes mathlib4#2089 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.algebra.order.extend_from: Yes mathlib4#2128 0a0ec35061ed9960bf0e7ffb0335f44447b58977
topology.algebra.order.extr_closure: Yes mathlib4#2096 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.algebra.order.field: Yes mathlib4#2626 9a59dcb7a2d06bf55da57b9030169219980660cd
topology.algebra.order.filter: Yes mathlib4#2167 98e83c3d541c77cdb7da20d79611a780ff8e7d90
topology.algebra.order.floor: Yes mathlib4#2485 84dc0bd6619acaea625086d6f53cb35cdd554219
topology.algebra.order.group: Yes mathlib4#2426 84dc0bd6619acaea625086d6f53cb35cdd554219
topology.algebra.order.intermediate_value: Yes mathlib4#2085 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.algebra.order.left_right: Yes mathlib4#1931 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.algebra.order.left_right_lim: Yes mathlib4#2131 0a0ec35061ed9960bf0e7ffb0335f44447b58977
topology.algebra.order.liminf_limsup: Yes mathlib4#2161 98e83c3d541c77cdb7da20d79611a780ff8e7d90
topology.algebra.order.monotone_continuity: Yes mathlib4#2098 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.algebra.order.monotone_convergence: Yes mathlib4#2097 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.algebra.order.proj_Icc: Yes mathlib4#2115 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.algebra.order.t5: Yes mathlib4#2102 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.algebra.order.upper_lower: Yes mathlib4#2503 992efbda6f85a5c9074375d3c7cb9764c64d8f72
topology.algebra.polynomial: 'No'
topology.algebra.ring.basic: Yes mathlib4#2614 9a59dcb7a2d06bf55da57b9030169219980660cd
topology.algebra.ring.ideal: Yes mathlib4#2754 9a59dcb7a2d06bf55da57b9030169219980660cd
topology.algebra.semigroup: Yes mathlib4#2080 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.algebra.star: Yes mathlib4#2094 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.algebra.star_subalgebra: 'No'
topology.algebra.uniform_convergence: 'No'
topology.algebra.uniform_field: No mathlib4#3049 f2ce6086713c78a7f880485f7917ea547a215982
topology.algebra.uniform_filter_basis: 'No'
topology.algebra.uniform_group: Yes mathlib4#2480 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.algebra.uniform_mul_action: Yes mathlib4#2499 70fd9563a21e7b963887c9360bd29b2393e6225a
topology.algebra.uniform_ring: Yes mathlib4#2789 9a59dcb7a2d06bf55da57b9030169219980660cd
topology.algebra.valuation: 'No'
topology.algebra.valued_field: 'No'
topology.algebra.with_zero_topology: Yes mathlib4#2703 3e0c4d76b6ebe9dfafb67d16f7286d2731ed6064
topology.bases: Yes mathlib4#1910 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.basic: Yes mathlib4#1826 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.bornology.basic: Yes mathlib4#1822 8631e2d5ea77f6c13054d9151d82b83069680cb1
topology.bornology.constructions: Yes mathlib4#1854 e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
topology.bornology.hom: Yes mathlib4#1855 e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
topology.category.Born: Yes mathlib4#2973 2143571557740bf69d0631339deea0d0e479df54
topology.category.CompHaus.basic: 'No'
topology.category.CompHaus.projective: 'No'
topology.category.Compactum: 'No'
topology.category.Locale: 'No'
topology.category.Profinite.as_limit: 'No'
topology.category.Profinite.basic: 'No'
topology.category.Profinite.cofiltered_limit: 'No'
topology.category.Profinite.projective: 'No'
topology.category.Top.adjunctions: 'No'
topology.category.Top.basic: No mathlib4#2993 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.category.Top.epi_mono: 'No'
topology.category.Top.limits: 'No'
topology.category.Top.open_nhds: 'No'
topology.category.Top.opens: 'No'
topology.category.TopCommRing: 'No'
topology.category.UniformSpace: 'No'
topology.compact_open: Yes mathlib4#2123 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.connected: Yes mathlib4#1934 d101e93197bb5f6ea89bd7ba386b7f7dff1f3903
topology.constructions: Yes mathlib4#1906 0c1f285a9f6e608ae2bdffa3f993eafb01eba829
topology.continuous_function.algebra: 'No'
topology.continuous_function.basic: Yes mathlib4#2053 6efec6bb9fcaed3cf1baaddb2eaadd8a2a06679c
topology.continuous_function.bounded: 'No'
topology.continuous_function.cocompact_map: Yes mathlib4#2130 0a0ec35061ed9960bf0e7ffb0335f44447b58977
topology.continuous_function.compact: 'No'
topology.continuous_function.ideals: 'No'
topology.continuous_function.locally_constant: 'No'
topology.continuous_function.ordered: Yes mathlib4#2448 84dc0bd6619acaea625086d6f53cb35cdd554219
topology.continuous_function.polynomial: 'No'
topology.continuous_function.stone_weierstrass: 'No'
topology.continuous_function.t0_sierpinski: Yes mathlib4#2240 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.continuous_function.units: 'No'
topology.continuous_function.weierstrass: 'No'
topology.continuous_function.zero_at_infty: 'No'
topology.continuous_on: Yes mathlib4#1907 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.covering: Yes mathlib4#3031 b8c810e2aac4a30bf8cda1e1c38d4f2e6065b2e7
topology.dense_embedding: Yes mathlib4#2003 d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
topology.discrete_quotient: Yes mathlib4#2157 d101e93197bb5f6ea89bd7ba386b7f7dff1f3903
topology.extend_from: Yes mathlib4#2055 b363547b3113d350d053abdf2884e9850a56b205
topology.fiber_bundle.basic: Yes mathlib4#2862 be2c24f56783935652cefffb4bfca7e4b25d167e
topology.fiber_bundle.constructions: 'No'
topology.fiber_bundle.is_homeomorphic_trivial_bundle: Yes mathlib4#2132 0a0ec35061ed9960bf0e7ffb0335f44447b58977
topology.fiber_bundle.trivialization: Yes mathlib4#2707 f2ce6086713c78a7f880485f7917ea547a215982
topology.filter: Yes mathlib4#2117 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.gluing: 'No'
topology.hom.open: Yes mathlib4#2172 98e83c3d541c77cdb7da20d79611a780ff8e7d90
topology.homeomorph: Yes mathlib4#2004 3b267e70a936eebb21ab546f49a8df34dd300b25
topology.homotopy.basic: Yes mathlib4#2825 11c53f174270aa43140c0b26dabce5fc4a253e80
topology.homotopy.contractible: 'No'
topology.homotopy.equiv: Yes mathlib4#2919 3d7987cda72abc473c7cdbbb075170e9ac620042
topology.homotopy.homotopy_group: 'No'
topology.homotopy.path: 'No'
topology.homotopy.product: 'No'
topology.inseparable: Yes mathlib4#1908 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.instances.add_circle: 'No'
topology.instances.complex: 'No'
topology.instances.discrete: 'No'
topology.instances.ennreal: Yes mathlib4#2734 90ac7a91781abbb5f0206888d68bd095f88c4229
topology.instances.ereal: Yes mathlib4#2796 f2ce6086713c78a7f880485f7917ea547a215982
topology.instances.int: Yes mathlib4#2612 70fd9563a21e7b963887c9360bd29b2393e6225a
topology.instances.irrational: 'No'
topology.instances.matrix: 'No'
topology.instances.nat: Yes mathlib4#2616 620af85adf5cd4282f962eb060e6e562e3e0c0ba
topology.instances.nnreal: Yes mathlib4#2672 32253a1a1071173b33dc7d6a218cf722c6feb514
topology.instances.rat: Yes mathlib4#2643 560891c425c743b1a25d4f8447cce6dd60947c1a
topology.instances.rat_lemmas: 'No'
topology.instances.real: Yes mathlib4#2633 9a59dcb7a2d06bf55da57b9030169219980660cd
topology.instances.real_vector_space: 'No'
topology.instances.sign: Yes mathlib4#2100 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.instances.triv_sq_zero_ext: 'No'
topology.is_locally_homeomorph: Yes mathlib4#2382 e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
topology.list: Yes mathlib4#2287 48085f140e684306f9e7da907cd5932056d1aded
topology.local_at_target: No mathlib4#2205 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.local_extr: Yes mathlib4#1909 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.local_homeomorph: Yes mathlib4#2231 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.locally_constant.algebra: Yes mathlib4#2592 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.locally_constant.basic: Yes mathlib4#2141 0a0ec35061ed9960bf0e7ffb0335f44447b58977
topology.locally_finite: Yes mathlib4#1877 f2ce6086713c78a7f880485f7917ea547a215982
topology.maps: Yes mathlib4#1873 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.metric_space.algebra: Yes mathlib4#2660 14d34b71b6d896b6e5f1ba2ec9124b9cd1f90fca
topology.metric_space.antilipschitz: Yes mathlib4#2635 97f079b7e89566de3a1143f887713667328c38ba
topology.metric_space.baire: 'No'
topology.metric_space.basic: Yes mathlib4#2425 195fcd60ff2bfe392543bceb0ec2adcdb472db4c
topology.metric_space.cau_seq_filter: Yes mathlib4#2852 f2ce6086713c78a7f880485f7917ea547a215982
topology.metric_space.closeds: 'No'
topology.metric_space.completion: Yes mathlib4#2756 f2ce6086713c78a7f880485f7917ea547a215982
topology.metric_space.contracting: 'No'
topology.metric_space.emetric_paracompact: Yes mathlib4#2599 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
topology.metric_space.emetric_space: Yes mathlib4#2407 195fcd60ff2bfe392543bceb0ec2adcdb472db4c
topology.metric_space.equicontinuity: Yes mathlib4#2638 f2ce6086713c78a7f880485f7917ea547a215982
topology.metric_space.gluing: Yes mathlib4#2711 e1a7bdeb4fd826b7e71d130d34988f0a2d26a177
topology.metric_space.gromov_hausdorff: 'No'
topology.metric_space.gromov_hausdorff_realized: 'No'
topology.metric_space.hausdorff_dimension: 'No'
topology.metric_space.hausdorff_distance: 'No'
topology.metric_space.holder: 'No'
topology.metric_space.infsep: Yes mathlib4#2613 5316314b553dcf8c6716541851517c1a9715e22b
topology.metric_space.isometric_smul: Yes mathlib4#2675 832a8ba8f10f11fea99367c469ff802e69a5b8ec
topology.metric_space.isometry: Yes mathlib4#2651 832a8ba8f10f11fea99367c469ff802e69a5b8ec
topology.metric_space.kuratowski: 'No'
topology.metric_space.lipschitz: Yes mathlib4#2634 f2ce6086713c78a7f880485f7917ea547a215982
topology.metric_space.metric_separated: Yes mathlib4#2608 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
topology.metric_space.metrizable: 'No'
topology.metric_space.metrizable_uniformity: 'No'
topology.metric_space.partition_of_unity: 'No'
topology.metric_space.pi_nat: 'No'
topology.metric_space.polish: 'No'
topology.metric_space.shrinking_lemma: Yes mathlib4#2629 f2ce6086713c78a7f880485f7917ea547a215982
topology.metric_space.thickened_indicator: 'No'
topology.nhds_set: Yes mathlib4#1875 f2ce6086713c78a7f880485f7917ea547a215982
topology.noetherian_space: Yes mathlib4#2219 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.omega_complete_partial_order: Yes mathlib4#2034 2705404e701abc6b3127da906f40bae062a169c9
topology.order: Yes mathlib4#1843 bcfa726826abd57587355b4b5b7e78ad6527b7e4
topology.order.basic: Yes mathlib4#2052 c985ae9840e06836a71db38de372f20acb49b790
topology.order.hom.basic: Yes mathlib4#2138 0a0ec35061ed9960bf0e7ffb0335f44447b58977
topology.order.hom.esakia: 'No'
topology.order.lattice: Yes mathlib4#2129 0a0ec35061ed9960bf0e7ffb0335f44447b58977
topology.order.lower_topology: Yes mathlib4#2163 98e83c3d541c77cdb7da20d79611a780ff8e7d90
topology.order.priestley: Yes mathlib4#2070 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.paracompact: Yes mathlib4#2036 2705404e701abc6b3127da906f40bae062a169c9
topology.partial: Yes mathlib4#2081 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.partition_of_unity: 'No'
topology.path_connected: Yes mathlib4#2755 f2ce6086713c78a7f880485f7917ea547a215982
topology.perfect: Yes mathlib4#2069 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.quasi_separated: Yes mathlib4#2261 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.semicontinuous: Yes mathlib4#2856 f2ce6086713c78a7f880485f7917ea547a215982
topology.separation: Yes mathlib4#1940 195fcd60ff2bfe392543bceb0ec2adcdb472db4c
topology.sequences: Yes mathlib4#2604 f2ce6086713c78a7f880485f7917ea547a215982
topology.sets.closeds: Yes mathlib4#2216 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.sets.compacts: Yes mathlib4#2265 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.sets.opens: Yes mathlib4#2118 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.sets.order: Yes mathlib4#2232 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.sheaves.abelian: 'No'
topology.sheaves.forget: 'No'
topology.sheaves.functors: 'No'
topology.sheaves.limits: 'No'
topology.sheaves.local_predicate: 'No'
topology.sheaves.locally_surjective: 'No'
topology.sheaves.operations: 'No'
topology.sheaves.presheaf: 'No'
topology.sheaves.presheaf_of_functions: 'No'
topology.sheaves.punit: 'No'
topology.sheaves.sheaf: 'No'
topology.sheaves.sheaf_condition.equalizer_products: 'No'
topology.sheaves.sheaf_condition.opens_le_cover: 'No'
topology.sheaves.sheaf_condition.pairwise_intersections: 'No'
topology.sheaves.sheaf_condition.sites: 'No'
topology.sheaves.sheaf_condition.unique_gluing: 'No'
topology.sheaves.sheaf_of_functions: 'No'
topology.sheaves.sheafify: 'No'
topology.sheaves.skyscraper: 'No'
topology.sheaves.stalks: 'No'
topology.shrinking_lemma: Yes mathlib4#2068 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.sober: Yes mathlib4#2134 0a0ec35061ed9960bf0e7ffb0335f44447b58977
topology.spectral.hom: Yes mathlib4#2127 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.stone_cech: Yes mathlib4#2147 0a0ec35061ed9960bf0e7ffb0335f44447b58977
topology.subset_properties: Yes mathlib4#1913 59694bd07f0a39c5beccba34bd9f413a160782bf
topology.support: Yes mathlib4#2002 d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
topology.tactic: Yes mathlib4#2481 79abf670d5f946912964c232736e97a761f29ebb Contains
  the `continuity` tactic, which is now in `Tactic.Continuity`
topology.tietze_extension: 'No'
topology.uniform_space.absolute_value: Yes mathlib4#2044 e1a7bdeb4fd826b7e71d130d34988f0a2d26a177
topology.uniform_space.abstract_completion: Yes mathlib4#2238 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.uniform_space.basic: Yes mathlib4#1993 195fcd60ff2bfe392543bceb0ec2adcdb472db4c
topology.uniform_space.cauchy: Yes mathlib4#2007 22131150f88a2d125713ffa0f4693e3355b1eb49
topology.uniform_space.compact: Yes mathlib4#2472 735b22f8f9ff9792cf4212d7cb051c4c994bc685
topology.uniform_space.compact_convergence: Yes mathlib4#2281 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.uniform_space.compare_reals: Yes mathlib4#2702 e1a7bdeb4fd826b7e71d130d34988f0a2d26a177
topology.uniform_space.complete_separated: Yes mathlib4#2063 b363547b3113d350d053abdf2884e9850a56b205
topology.uniform_space.completion: Yes mathlib4#2269 dc6c365e751e34d100e80fe6e314c3c3e0fd2988
topology.uniform_space.equicontinuity: Yes mathlib4#2457 f2ce6086713c78a7f880485f7917ea547a215982
topology.uniform_space.equiv: Yes mathlib4#2092 4c19a16e4b705bf135cf9a80ac18fcc99c438514
topology.uniform_space.matrix: 'No'
topology.uniform_space.pi: Yes mathlib4#2048 2705404e701abc6b3127da906f40bae062a169c9
topology.uniform_space.separation: Yes mathlib4#2014 0c1f285a9f6e608ae2bdffa3f993eafb01eba829
topology.uniform_space.uniform_convergence: Yes mathlib4#2051 2705404e701abc6b3127da906f40bae062a169c9
topology.uniform_space.uniform_convergence_topology: Yes mathlib4#2159 98e83c3d541c77cdb7da20d79611a780ff8e7d90
topology.uniform_space.uniform_embedding: Yes mathlib4#2038 195fcd60ff2bfe392543bceb0ec2adcdb472db4c
topology.unit_interval: Yes mathlib4#2684 f2ce6086713c78a7f880485f7917ea547a215982
topology.urysohns_bounded: 'No'
topology.urysohns_lemma: 'No'
topology.vector_bundle.basic: 'No'
topology.vector_bundle.constructions: 'No'
topology.vector_bundle.hom: 'No'