chore(*): add mathlib4 synchronization comments #2
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
3f5dc75
to
0afff13
Compare
e6ba7d4
to
03296e0
Compare
6a188e3
to
1e6598c
Compare
614c981
to
4e87719
Compare
df9fc62
to
f4c6dad
Compare
36b1c33
to
0c063ec
Compare
dea554d
to
abcde53
Compare
55c4a25
to
c012990
Compare
c012990
to
ba0a61b
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Regenerated from the port status wiki page.
Relates to the following files:
algebra.algebra.basicalgebra.algebra.bilinearalgebra.algebra.equivalgebra.algebra.homalgebra.algebra.operationsalgebra.algebra.pialgebra.algebra.prodalgebra.algebra.restrict_scalarsalgebra.algebra.spectrumalgebra.algebra.subalgebra.basicalgebra.algebra.subalgebra.pointwisealgebra.algebra.subalgebra.toweralgebra.algebra.toweralgebra.algebra.unitizationalgebra.algebraic_cardalgebra.big_operators.norm_numalgebra.category.Algebra.basicalgebra.category.Algebra.limitsalgebra.category.BoolRingalgebra.category.Group.Z_Module_equivalencealgebra.category.Group.abelianalgebra.category.Group.adjunctionsalgebra.category.Group.basicalgebra.category.Group.biproductsalgebra.category.Group.colimitsalgebra.category.Group.epi_monoalgebra.category.Group.equivalence_Group_AddGroupalgebra.category.Group.filtered_colimitsalgebra.category.Group.imagesalgebra.category.Group.injectivealgebra.category.Group.limitsalgebra.category.Group.preadditivealgebra.category.Group.subobjectalgebra.category.Group.zeroalgebra.category.GroupWithZeroalgebra.category.Module.abelianalgebra.category.Module.adjunctionsalgebra.category.Module.algebraalgebra.category.Module.basicalgebra.category.Module.biproductsalgebra.category.Module.change_of_ringsalgebra.category.Module.colimitsalgebra.category.Module.epi_monoalgebra.category.Module.filtered_colimitsalgebra.category.Module.imagesalgebra.category.Module.kernelsalgebra.category.Module.limitsalgebra.category.Module.productsalgebra.category.Module.projectivealgebra.category.Module.simplealgebra.category.Module.subobjectalgebra.category.Module.tannakaalgebra.category.Mon.adjunctionsalgebra.category.Mon.basicalgebra.category.Mon.colimitsalgebra.category.Mon.filtered_colimitsalgebra.category.Mon.limitsalgebra.category.Ring.adjunctionsalgebra.category.Ring.basicalgebra.category.Ring.colimitsalgebra.category.Ring.constructionsalgebra.category.Ring.filtered_colimitsalgebra.category.Ring.instancesalgebra.category.Ring.limitsalgebra.category.Semigroup.basicalgebra.category.fgModule.basicalgebra.category.fgModule.limitsalgebra.char_p.algebraalgebra.char_p.basicalgebra.char_p.char_and_cardalgebra.char_p.exp_charalgebra.char_p.invertiblealgebra.char_p.local_ringalgebra.char_p.mixed_char_zeroalgebra.char_p.pialgebra.char_p.quotientalgebra.char_p.subringalgebra.char_p.twoalgebra.continued_fractions.basicalgebra.continued_fractions.computation.approximation_corollariesalgebra.continued_fractions.computation.approximationsalgebra.continued_fractions.computation.basicalgebra.continued_fractions.computation.correctness_terminatingalgebra.continued_fractions.computation.terminates_iff_ratalgebra.continued_fractions.computation.translationsalgebra.continued_fractions.continuants_recurrencealgebra.continued_fractions.convergents_equivalgebra.continued_fractions.terminated_stablealgebra.continued_fractions.translationsalgebra.cubic_discriminantalgebra.direct_limitalgebra.direct_sum.algebraalgebra.direct_sum.decompositionalgebra.direct_sum.finsuppalgebra.direct_sum.internalalgebra.direct_sum.modulealgebra.direct_sum.ringalgebra.dual_numberalgebra.free_algebraalgebra.free_non_unital_non_assoc_algebraalgebra.gcd_monoid.divalgebra.gcd_monoid.integrally_closedalgebra.group_ring_action.invariantalgebra.hom.non_unital_algalgebra.homology.Modulealgebra.homology.additivealgebra.homology.augmentalgebra.homology.differential_objectalgebra.homology.exactalgebra.homology.flipalgebra.homology.functoralgebra.homology.homological_complexalgebra.homology.homologyalgebra.homology.homotopyalgebra.homology.homotopy_categoryalgebra.homology.image_to_kernelalgebra.homology.oppositealgebra.homology.quasi_isoalgebra.homology.short_exact.abelianalgebra.homology.short_exact.preadditivealgebra.homology.singlealgebra.jordan.basicalgebra.lie.abelianalgebra.lie.base_changealgebra.lie.basicalgebra.lie.cartan_matrixalgebra.lie.cartan_subalgebraalgebra.lie.characteralgebra.lie.classicalalgebra.lie.direct_sumalgebra.lie.engelalgebra.lie.freealgebra.lie.ideal_operationsalgebra.lie.matrixalgebra.lie.nilpotentalgebra.lie.non_unital_non_assoc_algebraalgebra.lie.normalizeralgebra.lie.of_associativealgebra.lie.quotientalgebra.lie.semisimplealgebra.lie.skew_adjointalgebra.lie.solvablealgebra.lie.subalgebraalgebra.lie.submodulealgebra.lie.tensor_productalgebra.lie.universal_envelopingalgebra.lie.weightsalgebra.linear_recurrencealgebra.module.algebraalgebra.module.bimodulealgebra.module.dedekind_domainalgebra.module.graded_modulealgebra.module.injectivealgebra.module.localized_modulealgebra.module.pidalgebra.module.projectivealgebra.module.submodule.bilinearalgebra.module.submodule.pointwisealgebra.module.torsionalgebra.monoid_algebra.basicalgebra.monoid_algebra.degreealgebra.monoid_algebra.gradingalgebra.monoid_algebra.no_zero_divisorsalgebra.monoid_algebra.supportalgebra.monoid_algebra.to_direct_sumalgebra.order.algebraalgebra.order.chebyshevalgebra.order.complete_fieldalgebra.order.hom.ringalgebra.order.intervalalgebra.order.rearrangementalgebra.order.to_interval_modalgebra.polynomial.big_operatorsalgebra.polynomial.group_ring_actionalgebra.quadratic_discriminantalgebra.quaternionalgebra.quaternion_basisalgebra.ring.boolean_ringalgebra.ring_quotalgebra.squarefreealgebra.star.chshalgebra.star.freealgebra.star.modulealgebra.star.star_alg_homalgebra.star.subalgebraalgebra.symmetrizedalgebra.triv_sq_zero_extalgebraic_geometry.AffineSchemealgebraic_geometry.Gamma_Spec_adjunctionalgebraic_geometry.Schemealgebraic_geometry.Specalgebraic_geometry.elliptic_curve.pointalgebraic_geometry.elliptic_curve.weierstrassalgebraic_geometry.function_fieldalgebraic_geometry.gluingalgebraic_geometry.limitsalgebraic_geometry.locally_ringed_spacealgebraic_geometry.locally_ringed_space.has_colimitsalgebraic_geometry.morphisms.basicalgebraic_geometry.morphisms.finite_typealgebraic_geometry.morphisms.open_immersionalgebraic_geometry.morphisms.quasi_compactalgebraic_geometry.morphisms.quasi_separatedalgebraic_geometry.morphisms.ring_hom_propertiesalgebraic_geometry.morphisms.universally_closedalgebraic_geometry.presheafed_spacealgebraic_geometry.presheafed_space.gluingalgebraic_geometry.presheafed_space.has_colimitsalgebraic_geometry.prime_spectrum.basicalgebraic_geometry.prime_spectrum.is_open_comap_Calgebraic_geometry.prime_spectrum.maximalalgebraic_geometry.prime_spectrum.noetherianalgebraic_geometry.projective_spectrum.schemealgebraic_geometry.projective_spectrum.structure_sheafalgebraic_geometry.projective_spectrum.topologyalgebraic_geometry.propertiesalgebraic_geometry.pullbacksalgebraic_geometry.ringed_spacealgebraic_geometry.sheafed_spacealgebraic_geometry.stalksalgebraic_geometry.structure_sheafalgebraic_topology.Moore_complexalgebraic_topology.alternating_face_map_complexalgebraic_topology.cech_nervealgebraic_topology.dold_kan.decompositionalgebraic_topology.dold_kan.degeneraciesalgebraic_topology.dold_kan.equivalence_additivealgebraic_topology.dold_kan.facesalgebraic_topology.dold_kan.functor_gammaalgebraic_topology.dold_kan.functor_nalgebraic_topology.dold_kan.gamma_comp_nalgebraic_topology.dold_kan.homotopiesalgebraic_topology.dold_kan.homotopy_equivalencealgebraic_topology.dold_kan.n_comp_gammaalgebraic_topology.dold_kan.n_reflects_isoalgebraic_topology.dold_kan.normalizedalgebraic_topology.dold_kan.notationsalgebraic_topology.dold_kan.p_inftyalgebraic_topology.dold_kan.projectionsalgebraic_topology.dold_kan.split_simplicial_objectalgebraic_topology.extra_degeneracyalgebraic_topology.fundamental_groupoid.basicalgebraic_topology.fundamental_groupoid.fundamental_groupalgebraic_topology.fundamental_groupoid.induced_mapsalgebraic_topology.fundamental_groupoid.productalgebraic_topology.fundamental_groupoid.punitalgebraic_topology.fundamental_groupoid.simply_connectedalgebraic_topology.nervealgebraic_topology.simplex_categoryalgebraic_topology.simplicial_objectalgebraic_topology.simplicial_setalgebraic_topology.split_simplicial_objectalgebraic_topology.topological_simplexanalysis.ODE.gronwallanalysis.ODE.picard_lindelofanalysis.analytic.basicanalysis.analytic.compositionanalysis.analytic.inverseanalysis.analytic.isolated_zerosanalysis.analytic.linearanalysis.analytic.radius_liminfanalysis.analytic.uniquenessanalysis.asymptotics.asymptotic_equivalentanalysis.asymptotics.asymptoticsanalysis.asymptotics.specific_asymptoticsanalysis.asymptotics.superpolynomial_decayanalysis.asymptotics.thetaanalysis.bounded_variationanalysis.box_integral.basicanalysis.box_integral.box.basicanalysis.box_integral.box.subbox_inductionanalysis.box_integral.divergence_theoremanalysis.box_integral.integrabilityanalysis.box_integral.partition.additiveanalysis.box_integral.partition.basicanalysis.box_integral.partition.filteranalysis.box_integral.partition.measureanalysis.box_integral.partition.splitanalysis.box_integral.partition.subbox_inductionanalysis.box_integral.partition.taggedanalysis.calculus.affine_mapanalysis.calculus.bump_function_findimanalysis.calculus.bump_function_inneranalysis.calculus.conformal.inner_productanalysis.calculus.conformal.normed_spaceanalysis.calculus.cont_diffanalysis.calculus.darbouxanalysis.calculus.diff_cont_on_clanalysis.calculus.dslopeanalysis.calculus.extend_derivanalysis.calculus.fderiv_analyticanalysis.calculus.fderiv_measurableanalysis.calculus.fderiv_symmetricanalysis.calculus.formal_multilinear_seriesanalysis.calculus.implicitanalysis.calculus.inverseanalysis.calculus.iterated_derivanalysis.calculus.lagrange_multipliersanalysis.calculus.lhopitalanalysis.calculus.local_extranalysis.calculus.mean_valueanalysis.calculus.monotoneanalysis.calculus.parametric_integralanalysis.calculus.parametric_interval_integralanalysis.calculus.seriesanalysis.calculus.tangent_coneanalysis.calculus.tayloranalysis.calculus.uniform_limits_derivanalysis.complex.abs_maxanalysis.complex.arganalysis.complex.basicanalysis.complex.cauchy_integralanalysis.complex.circleanalysis.complex.conformalanalysis.complex.isometryanalysis.complex.liouvilleanalysis.complex.locally_uniform_limitanalysis.complex.open_mappinganalysis.complex.operator_normanalysis.complex.phragmen_lindelofanalysis.complex.polynomialanalysis.complex.re_im_topologyanalysis.complex.real_derivanalysis.complex.removable_singularityanalysis.complex.schwarzanalysis.complex.unit_disc.basicanalysis.complex.upper_half_plane.basicanalysis.complex.upper_half_plane.functions_bounded_at_inftyanalysis.complex.upper_half_plane.metricanalysis.complex.upper_half_plane.topologyanalysis.constant_speedanalysis.convex.basicanalysis.convex.betweenanalysis.convex.bodyanalysis.convex.caratheodoryanalysis.convex.combinationanalysis.convex.complexanalysis.convex.cone.basicanalysis.convex.contractibleanalysis.convex.exposedanalysis.convex.extremaanalysis.convex.extremeanalysis.convex.functionanalysis.convex.gaugeanalysis.convex.hullanalysis.convex.independentanalysis.convex.integralanalysis.convex.intrinsicanalysis.convex.jensenanalysis.convex.joinanalysis.convex.krein_milmananalysis.convex.measureanalysis.convex.normedanalysis.convex.partition_of_unityanalysis.convex.quasiconvexanalysis.convex.segmentanalysis.convex.sideanalysis.convex.simplicial_complex.basicanalysis.convex.slopeanalysis.convex.staranalysis.convex.stone_separationanalysis.convex.strictanalysis.convex.strict_convex_betweenanalysis.convex.strict_convex_spaceanalysis.convex.topologyanalysis.convex.uniformanalysis.convolutionanalysis.fourier.add_circleanalysis.fourier.riemann_lebesgue_lemmaanalysis.hoferanalysis.inner_product_space.adjointanalysis.inner_product_space.basicanalysis.inner_product_space.calculusanalysis.inner_product_space.conformal_linear_mapanalysis.inner_product_space.dualanalysis.inner_product_space.euclidean_distanalysis.inner_product_space.gram_schmidt_orthoanalysis.inner_product_space.l2_spaceanalysis.inner_product_space.lax_milgramanalysis.inner_product_space.orientationanalysis.inner_product_space.pi_L2analysis.inner_product_space.positiveanalysis.inner_product_space.projectionanalysis.inner_product_space.rayleighanalysis.inner_product_space.spectrumanalysis.inner_product_space.symmetricanalysis.inner_product_space.two_dimanalysis.locally_convex.abs_convexanalysis.locally_convex.balanced_core_hullanalysis.locally_convex.basicanalysis.locally_convex.boundedanalysis.locally_convex.continuous_of_boundedanalysis.locally_convex.polaranalysis.locally_convex.weak_dualanalysis.locally_convex.with_seminormsanalysis.matrixanalysis.mean_inequalitiesanalysis.mean_inequalities_powanalysis.normed.field.basicanalysis.normed.field.infinite_sumanalysis.normed.field.unit_ballanalysis.normed.group.SemiNormedGroupanalysis.normed.group.SemiNormedGroup.completionanalysis.normed.group.SemiNormedGroup.kernelsanalysis.normed.group.add_circleanalysis.normed.group.add_torsoranalysis.normed.group.ball_sphereanalysis.normed.group.basicanalysis.normed.group.completionanalysis.normed.group.controlled_closureanalysis.normed.group.homanalysis.normed.group.hom_completionanalysis.normed.group.infinite_sumanalysis.normed.group.pointwiseanalysis.normed.group.quotientanalysis.normed.group.seminormanalysis.normed.order.basicanalysis.normed.order.latticeanalysis.normed.ring.seminormanalysis.normed_space.M_structureanalysis.normed_space.add_torsoranalysis.normed_space.add_torsor_basesanalysis.normed_space.affine_isometryanalysis.normed_space.algebraanalysis.normed_space.ball_actionanalysis.normed_space.banachanalysis.normed_space.banach_steinhausanalysis.normed_space.basicanalysis.normed_space.bounded_linear_mapsanalysis.normed_space.compact_operatoranalysis.normed_space.complementedanalysis.normed_space.completionanalysis.normed_space.conformal_linear_mapanalysis.normed_space.continuous_affine_mapanalysis.normed_space.continuous_linear_mapanalysis.normed_space.dualanalysis.normed_space.dual_numberanalysis.normed_space.enormanalysis.normed_space.exponentialanalysis.normed_space.extendanalysis.normed_space.extranalysis.normed_space.finite_dimensionanalysis.normed_space.hahn_banach.extensionanalysis.normed_space.hahn_banach.separationanalysis.normed_space.indicator_functionanalysis.normed_space.intanalysis.normed_space.is_R_or_Canalysis.normed_space.linear_isometryanalysis.normed_space.lp_equivanalysis.normed_space.lp_spaceanalysis.normed_space.matrix_exponentialanalysis.normed_space.mazur_ulamanalysis.normed_space.multilinearanalysis.normed_space.operator_normanalysis.normed_space.pi_Lpanalysis.normed_space.pointwiseanalysis.normed_space.rayanalysis.normed_space.riesz_lemmaanalysis.normed_space.spectrumanalysis.normed_space.star.basicanalysis.normed_space.star.exponentialanalysis.normed_space.star.gelfand_dualityanalysis.normed_space.star.matrixanalysis.normed_space.star.mulanalysis.normed_space.star.spectrumanalysis.normed_space.triv_sq_zero_extanalysis.normed_space.unitsanalysis.normed_space.weak_dualanalysis.p_seriesanalysis.quaternionanalysis.schwartz_spaceanalysis.seminormanalysis.special_functions.arsinhanalysis.special_functions.bernsteinanalysis.special_functions.compare_expanalysis.special_functions.complex.arganalysis.special_functions.complex.circleanalysis.special_functions.complex.loganalysis.special_functions.complex.log_derivanalysis.special_functions.expanalysis.special_functions.exp_derivanalysis.special_functions.exponentialanalysis.special_functions.gaussiananalysis.special_functions.integralsanalysis.special_functions.japanese_bracketanalysis.special_functions.log.baseanalysis.special_functions.log.basicanalysis.special_functions.log.derivanalysis.special_functions.log.monotoneanalysis.special_functions.non_integrableanalysis.special_functions.polar_coordanalysis.special_functions.polynomialsanalysis.special_functions.sqrtanalysis.special_functions.stirlinganalysis.special_functions.trigonometric.angleanalysis.special_functions.trigonometric.arctananalysis.special_functions.trigonometric.arctan_derivanalysis.special_functions.trigonometric.basicanalysis.special_functions.trigonometric.boundsanalysis.special_functions.trigonometric.chebyshevanalysis.special_functions.trigonometric.complexanalysis.special_functions.trigonometric.complex_derivanalysis.special_functions.trigonometric.derivanalysis.special_functions.trigonometric.euler_sine_prodanalysis.special_functions.trigonometric.inverseanalysis.special_functions.trigonometric.inverse_derivanalysis.special_functions.trigonometric.seriesanalysis.specific_limits.basicanalysis.specific_limits.floor_powanalysis.specific_limits.normedanalysis.subadditiveanalysis.sum_integral_comparisonsanalysis.von_neumann_algebra.basiccategory_theory.Fintypecategory_theory.abelian.basiccategory_theory.abelian.diagram_lemmas.fourcategory_theory.abelian.exactcategory_theory.abelian.extcategory_theory.abelian.functor_categorycategory_theory.abelian.generatorcategory_theory.abelian.homologycategory_theory.abelian.imagescategory_theory.abelian.injectivecategory_theory.abelian.injective_resolutioncategory_theory.abelian.left_derivedcategory_theory.abelian.non_preadditivecategory_theory.abelian.oppositecategory_theory.abelian.projectivecategory_theory.abelian.pseudoelementscategory_theory.abelian.right_derivedcategory_theory.abelian.subobjectcategory_theory.abelian.transfercategory_theory.actioncategory_theory.adhesivecategory_theory.adjunction.adjoint_functor_theoremscategory_theory.adjunction.basiccategory_theory.adjunction.commacategory_theory.adjunction.evaluationcategory_theory.adjunction.fully_faithfulcategory_theory.adjunction.liftingcategory_theory.adjunction.limitscategory_theory.adjunction.matescategory_theory.adjunction.oppositescategory_theory.adjunction.overcategory_theory.adjunction.reflectivecategory_theory.adjunction.whiskeringcategory_theory.arrowcategory_theory.balancedcategory_theory.bicategory.Endcategory_theory.bicategory.coherencecategory_theory.bicategory.coherence_tacticcategory_theory.bicategory.freecategory_theory.bicategory.functorcategory_theory.bicategory.functor_bicategorycategory_theory.bicategory.locally_discretecategory_theory.bicategory.natural_transformationcategory_theory.bicategory.single_objcategory_theory.category.Bipointedcategory_theory.category.Catcategory_theory.category.Cat.limitcategory_theory.category.Groupoidcategory_theory.category.PartialFuncategory_theory.category.Pointedcategory_theory.category.Quivcategory_theory.category.Twopcategory_theory.category.galois_connectioncategory_theory.category.pairwisecategory_theory.category.preordercategory_theory.category.uliftcategory_theory.closed.cartesiancategory_theory.closed.functorcategory_theory.closed.functor_categorycategory_theory.closed.idealcategory_theory.closed.monoidalcategory_theory.closed.typescategory_theory.closed.zerocategory_theory.comm_sqcategory_theory.commacategory_theory.concrete_category.basiccategory_theory.concrete_category.bundled_homcategory_theory.concrete_category.elementwisecategory_theory.concrete_category.reflects_isomorphismscategory_theory.concrete_category.unbundled_homcategory_theory.conjcategory_theory.connected_componentscategory_theory.corecategory_theory.differential_objectcategory_theory.discrete_categorycategory_theory.elementscategory_theory.elementwisecategory_theory.endofunctor.algebracategory_theory.endomorphismcategory_theory.enriched.basiccategory_theory.epi_monocategory_theory.essentially_smallcategory_theory.extensivecategory_theory.filteredcategory_theory.fin_categorycategory_theory.functor.curryingcategory_theory.functor.epi_monocategory_theory.functor.flatcategory_theory.functor.homcategory_theory.functor.left_derivedcategory_theory.functor.reflects_isomorphismscategory_theory.generatorcategory_theory.glue_datacategory_theory.graded_objectcategory_theory.grothendieckcategory_theory.groupoidcategory_theory.groupoid.basiccategory_theory.groupoid.free_groupoidcategory_theory.groupoid.subgroupoidcategory_theory.groupoid.vertex_groupcategory_theory.idempotents.basiccategory_theory.idempotents.biproductscategory_theory.idempotents.functor_categoriescategory_theory.idempotents.functor_extensioncategory_theory.idempotents.homological_complexcategory_theory.idempotents.karoubicategory_theory.idempotents.karoubi_karoubicategory_theory.idempotents.simplicial_objectcategory_theory.is_connectedcategory_theory.isomorphism_classescategory_theory.lifting_properties.adjunctioncategory_theory.lifting_properties.basiccategory_theory.limits.biconescategory_theory.limits.colimit_limitcategory_theory.limits.commacategory_theory.limits.concrete_categorycategory_theory.limits.cone_categorycategory_theory.limits.conescategory_theory.limits.connectedcategory_theory.limits.constructions.binary_productscategory_theory.limits.constructions.epi_monocategory_theory.limits.constructions.equalizerscategory_theory.limits.constructions.filteredcategory_theory.limits.constructions.finite_products_of_binary_productscategory_theory.limits.constructions.limits_of_products_and_equalizerscategory_theory.limits.constructions.over.connectedcategory_theory.limits.constructions.over.productscategory_theory.limits.constructions.pullbackscategory_theory.limits.constructions.weakly_initialcategory_theory.limits.constructions.zero_objectscategory_theory.limits.createscategory_theory.limits.essentially_smallcategory_theory.limits.exact_functorcategory_theory.limits.filteredcategory_theory.limits.filtered_colimit_commutes_finite_limitcategory_theory.limits.finalcategory_theory.limits.fubinicategory_theory.limits.full_subcategorycategory_theory.limits.functor_categorycategory_theory.limits.has_limitscategory_theory.limits.is_limitcategory_theory.limits.kan_extensioncategory_theory.limits.latticecategory_theory.limits.mono_coprodcategory_theory.limits.oppositescategory_theory.limits.overcategory_theory.limits.picategory_theory.limits.preserves.basiccategory_theory.limits.preserves.filteredcategory_theory.limits.preserves.finitecategory_theory.limits.preserves.functor_categorycategory_theory.limits.preserves.limitscategory_theory.limits.preserves.oppositescategory_theory.limits.preserves.shapes.binary_productscategory_theory.limits.preserves.shapes.biproductscategory_theory.limits.preserves.shapes.equalizerscategory_theory.limits.preserves.shapes.imagescategory_theory.limits.preserves.shapes.kernelscategory_theory.limits.preserves.shapes.productscategory_theory.limits.preserves.shapes.pullbackscategory_theory.limits.preserves.shapes.terminalcategory_theory.limits.preserves.shapes.zerocategory_theory.limits.presheafcategory_theory.limits.shapes.binary_productscategory_theory.limits.shapes.biproductscategory_theory.limits.shapes.comm_sqcategory_theory.limits.shapes.diagonalcategory_theory.limits.shapes.disjoint_coproductcategory_theory.limits.shapes.equalizerscategory_theory.limits.shapes.equivalencecategory_theory.limits.shapes.finite_limitscategory_theory.limits.shapes.finite_productscategory_theory.limits.shapes.functor_categorycategory_theory.limits.shapes.imagescategory_theory.limits.shapes.kernel_paircategory_theory.limits.shapes.kernelscategory_theory.limits.shapes.multiequalizercategory_theory.limits.shapes.normal_mono.basiccategory_theory.limits.shapes.normal_mono.equalizerscategory_theory.limits.shapes.productscategory_theory.limits.shapes.pullbackscategory_theory.limits.shapes.reflexivecategory_theory.limits.shapes.regular_monocategory_theory.limits.shapes.split_coequalizercategory_theory.limits.shapes.strict_initialcategory_theory.limits.shapes.strong_epicategory_theory.limits.shapes.terminalcategory_theory.limits.shapes.typescategory_theory.limits.shapes.wide_equalizerscategory_theory.limits.shapes.wide_pullbackscategory_theory.limits.shapes.zero_morphismscategory_theory.limits.shapes.zero_objectscategory_theory.limits.small_completecategory_theory.limits.typescategory_theory.limits.unitcategory_theory.limits.yonedacategory_theory.linear.basiccategory_theory.linear.functor_categorycategory_theory.linear.linear_functorcategory_theory.linear.yonedacategory_theory.localization.constructioncategory_theory.localization.oppositecategory_theory.localization.predicatecategory_theory.monad.adjunctioncategory_theory.monad.algebracategory_theory.monad.basiccategory_theory.monad.coequalizercategory_theory.monad.equiv_moncategory_theory.monad.kleislicategory_theory.monad.limitscategory_theory.monad.monadicitycategory_theory.monad.productscategory_theory.monad.typescategory_theory.monoidal.Bimodcategory_theory.monoidal.CommMon_category_theory.monoidal.Endcategory_theory.monoidal.Mon_category_theory.monoidal.braidedcategory_theory.monoidal.categorycategory_theory.monoidal.centercategory_theory.monoidal.coherencecategory_theory.monoidal.coherence_lemmascategory_theory.monoidal.discretecategory_theory.monoidal.free.basiccategory_theory.monoidal.free.coherencecategory_theory.monoidal.functorcategory_theory.monoidal.functor_categorycategory_theory.monoidal.functorialcategory_theory.monoidal.internal.Modulecategory_theory.monoidal.internal.functor_categorycategory_theory.monoidal.internal.limitscategory_theory.monoidal.internal.typescategory_theory.monoidal.limitscategory_theory.monoidal.linearcategory_theory.monoidal.natural_transformationcategory_theory.monoidal.of_has_finite_productscategory_theory.monoidal.oppositecategory_theory.monoidal.preadditivecategory_theory.monoidal.rigid.basiccategory_theory.monoidal.rigid.functor_categorycategory_theory.monoidal.rigid.of_equivalencecategory_theory.monoidal.skeletoncategory_theory.monoidal.subcategorycategory_theory.monoidal.torcategory_theory.monoidal.transportcategory_theory.morphism_propertycategory_theory.noetheriancategory_theory.overcategory_theory.path_categorycategory_theory.pemptycategory_theory.pi.basiccategory_theory.preadditive.Matcategory_theory.preadditive.additive_functorcategory_theory.preadditive.basiccategory_theory.preadditive.biproductscategory_theory.preadditive.eilenberg_moorecategory_theory.preadditive.endo_functorcategory_theory.preadditive.functor_categorycategory_theory.preadditive.generatorcategory_theory.preadditive.hom_orthogonalcategory_theory.preadditive.injectivecategory_theory.preadditive.injective_resolutioncategory_theory.preadditive.left_exactcategory_theory.preadditive.of_biproductscategory_theory.preadditive.oppositecategory_theory.preadditive.projectivecategory_theory.preadditive.projective_resolutioncategory_theory.preadditive.schurcategory_theory.preadditive.single_objcategory_theory.products.associatorcategory_theory.products.basiccategory_theory.products.bifunctorcategory_theory.punitcategory_theory.quotientcategory_theory.simplecategory_theory.single_objcategory_theory.sites.adjunctioncategory_theory.sites.canonicalcategory_theory.sites.closedcategory_theory.sites.compatible_pluscategory_theory.sites.compatible_sheafificationcategory_theory.sites.cover_liftingcategory_theory.sites.cover_preservingcategory_theory.sites.dense_subsitecategory_theory.sites.grothendieckcategory_theory.sites.induced_topologycategory_theory.sites.left_exactcategory_theory.sites.limitscategory_theory.sites.pluscategory_theory.sites.pretopologycategory_theory.sites.sheafcategory_theory.sites.sheaf_of_typescategory_theory.sites.sheafificationcategory_theory.sites.sievescategory_theory.sites.spacescategory_theory.sites.subsheafcategory_theory.sites.surjectivecategory_theory.sites.typescategory_theory.sites.whiskeringcategory_theory.skeletalcategory_theory.structured_arrowcategory_theory.subobject.basiccategory_theory.subobject.commacategory_theory.subobject.factor_thrucategory_theory.subobject.latticecategory_theory.subobject.limitscategory_theory.subobject.mono_overcategory_theory.subobject.typescategory_theory.subobject.well_poweredcategory_theory.subterminalcategory_theory.sums.associatorcategory_theory.sums.basiccategory_theory.triangulated.basiccategory_theory.triangulated.pretriangulatedcategory_theory.triangulated.rotatecategory_theory.triangulated.triangulatedcategory_theory.typescategory_theory.with_terminalcategory_theory.yonedacombinatorics.additive.behrendcombinatorics.additive.pluennecke_ruzsacombinatorics.additive.salem_spencercombinatorics.catalancombinatorics.configurationcombinatorics.derangements.basiccombinatorics.derangements.exponentialcombinatorics.derangements.finitecombinatorics.hales_jewettcombinatorics.hall.basiccombinatorics.hindmancombinatorics.partitioncombinatorics.simple_graph.acycliccombinatorics.simple_graph.adj_matrixcombinatorics.simple_graph.basiccombinatorics.simple_graph.cliquecombinatorics.simple_graph.coloringcombinatorics.simple_graph.connectivitycombinatorics.simple_graph.degree_sumcombinatorics.simple_graph.densitycombinatorics.simple_graph.ends.defscombinatorics.simple_graph.ends.propertiescombinatorics.simple_graph.hassecombinatorics.simple_graph.inc_matrixcombinatorics.simple_graph.matchingcombinatorics.simple_graph.metriccombinatorics.simple_graph.partitioncombinatorics.simple_graph.prodcombinatorics.simple_graph.regularity.boundcombinatorics.simple_graph.regularity.energycombinatorics.simple_graph.regularity.uniformcombinatorics.simple_graph.strongly_regularcombinatorics.simple_graph.subgraphcombinatorics.simple_graph.trailscombinatorics.simple_graph.triangle.basiccomputability.DFAcomputability.NFAcomputability.ackermanncomputability.encodingcomputability.epsilon_NFAcomputability.haltingcomputability.languagecomputability.partreccomputability.partrec_codecomputability.primreccomputability.reducecomputability.regular_expressionscomputability.tm_computablecomputability.tm_to_partreccomputability.turing_machinecontrol.bifunctorcontrol.bitraversable.basiccontrol.bitraversable.instancescontrol.bitraversable.lemmascontrol.foldcontrol.lawful_fixcontrol.randomcontrol.uliftabledata.W.cardinaldata.analysis.topologydata.buffer.parser.basicdata.buffer.parser.numeraldata.complex.basicdata.complex.cardinalitydata.complex.determinantdata.complex.exponentialdata.complex.exponential_boundsdata.complex.moduledata.dfinsupp.multisetdata.dfinsupp.well_foundeddata.finset.intervaldata.finset.supsdata.finset.symdata.finsupp.lexdata.finsupp.well_foundeddata.fintype.arraydata.fintype.card_embeddingdata.fintype.quotientdata.hash_mapdata.is_R_or_C.basicdata.is_R_or_C.lemmasdata.jsondata.list.intervalsdata.matrix.basicdata.matrix.basisdata.matrix.blockdata.matrix.char_pdata.matrix.hadamarddata.matrix.kroneckerdata.matrix.notationdata.matrix.pequivdata.matrix.rankdata.multiset.intervaldata.mv_polynomial.basicdata.mv_polynomial.cardinaldata.mv_polynomial.comapdata.mv_polynomial.comm_ringdata.mv_polynomial.counitdata.mv_polynomial.derivationdata.mv_polynomial.equivdata.mv_polynomial.expanddata.mv_polynomial.funextdata.mv_polynomial.invertibledata.mv_polynomial.monaddata.mv_polynomial.pderivdata.mv_polynomial.renamedata.mv_polynomial.supporteddata.mv_polynomial.variablesdata.nat.choose.castdata.nat.choose.factorizationdata.nat.choose.multinomialdata.nat.choose.vandermondedata.nat.countdata.nat.digitsdata.nat.factorial.castdata.nat.factorization.basicdata.nat.factorization.prime_powdata.nat.multiplicitydata.nat.nthdata.nat.periodicdata.nat.prime_norm_numdata.nat.sqrt_norm_numdata.nat.squarefreedata.nat.totientdata.num.lemmasdata.num.primedata.ordmap.ordnodedata.ordmap.ordsetdata.pfunctor.multivariate.Mdata.pfunctor.multivariate.Wdata.pfunctor.multivariate.basicdata.pfunctor.univariate.Mdata.polynomial.algebra_mapdata.polynomial.basicdata.polynomial.cancel_leadsdata.polynomial.cardinaldata.polynomial.coeffdata.polynomial.degree.card_pow_degreedata.polynomial.degree.definitionsdata.polynomial.degree.lemmasdata.polynomial.degree.trailing_degreedata.polynomial.denoms_clearabledata.polynomial.derivativedata.polynomial.divdata.polynomial.erase_leaddata.polynomial.evaldata.polynomial.expanddata.polynomial.field_divisiondata.polynomial.hasse_derivdata.polynomial.identitiesdata.polynomial.inductiondata.polynomial.inductionsdata.polynomial.integral_normalizationdata.polynomial.laurentdata.polynomial.liftsdata.polynomial.mirrordata.polynomial.moduledata.polynomial.monicdata.polynomial.monomialdata.polynomial.partial_fractionsdata.polynomial.reversedata.polynomial.ring_divisiondata.polynomial.splitsdata.polynomial.taylordata.polynomial.unit_trinomialdata.qpf.multivariate.basicdata.qpf.multivariate.constructions.cofixdata.qpf.multivariate.constructions.compdata.qpf.multivariate.constructions.constdata.qpf.multivariate.constructions.fixdata.qpf.multivariate.constructions.prjdata.qpf.multivariate.constructions.quotdata.qpf.multivariate.constructions.sigmadata.qpf.univariate.basicdata.rat.nnratdata.real.cardinalitydata.real.conjugate_exponentsdata.real.enat_ennrealdata.real.ennrealdata.real.erealdata.real.golden_ratiodata.real.hyperrealdata.real.irrationaldata.real.nnrealdata.real.pi.boundsdata.real.pi.leibnizdata.real.pi.wallisdata.real.sqrtdata.string.basicdata.string.defsdata.sym.carddata.treedata.vector3data.zmod.algebradata.zmod.basicdata.zmod.coprimedata.zmod.paritydata.zmod.quotientdeprecated.subfielddeprecated.subringdynamics.circle.rotation_number.translation_numberdynamics.ergodic.add_circledynamics.ergodic.conservativedynamics.ergodic.ergodicdynamics.ergodic.measure_preservingdynamics.flowdynamics.omega_limitfield_theory.abel_ruffinifield_theory.adjoinfield_theory.cardinalityfield_theory.chevalley_warningfield_theory.finite.basicfield_theory.finite.galois_fieldfield_theory.finite.polynomialfield_theory.finite.tracefield_theory.finitenessfield_theory.fixedfield_theory.galoisfield_theory.intermediate_fieldfield_theory.is_alg_closed.algebraic_closurefield_theory.is_alg_closed.basicfield_theory.is_alg_closed.classificationfield_theory.krull_topologyfield_theory.laurentfield_theory.minpoly.basicfield_theory.minpoly.fieldfield_theory.minpoly.is_integrally_closedfield_theory.mv_polynomialfield_theory.normalfield_theory.perfect_closurefield_theory.polynomial_galois_groupfield_theory.primitive_elementfield_theory.ratfuncfield_theory.separablefield_theory.separable_degreefield_theory.subfieldfield_theory.towergeometry.euclidean.angle.oriented.affinegeometry.euclidean.angle.oriented.basicgeometry.euclidean.angle.oriented.right_anglegeometry.euclidean.angle.oriented.rotationgeometry.euclidean.angle.spheregeometry.euclidean.angle.unoriented.affinegeometry.euclidean.angle.unoriented.basicgeometry.euclidean.angle.unoriented.conformalgeometry.euclidean.angle.unoriented.right_anglegeometry.euclidean.basicgeometry.euclidean.circumcentergeometry.euclidean.inversiongeometry.euclidean.monge_pointgeometry.euclidean.trianglegeometry.manifold.algebra.left_invariant_derivationgeometry.manifold.algebra.lie_groupgeometry.manifold.algebra.monoidgeometry.manifold.algebra.smooth_functionsgeometry.manifold.algebra.structuresgeometry.manifold.bump_functiongeometry.manifold.charted_spacegeometry.manifold.complexgeometry.manifold.conformal_groupoidgeometry.manifold.cont_mdiffgeometry.manifold.cont_mdiff_mapgeometry.manifold.cont_mdiff_mfderivgeometry.manifold.derivation_bundlegeometry.manifold.diffeomorphgeometry.manifold.instances.realgeometry.manifold.instances.spheregeometry.manifold.instances.units_of_normed_algebrageometry.manifold.local_invariant_propertiesgeometry.manifold.metrizablegeometry.manifold.mfderivgeometry.manifold.partition_of_unitygeometry.manifold.smooth_manifold_with_cornersgeometry.manifold.whitney_embeddinggroup_theory.commensurablegroup_theory.commuting_probabilitygroup_theory.complementgroup_theory.exponentgroup_theory.finite_abeliangroup_theory.free_abelian_groupgroup_theory.free_abelian_group_finsuppgroup_theory.free_productgroup_theory.indexgroup_theory.nielsen_schreiergroup_theory.nilpotentgroup_theory.noncomm_pi_coprodgroup_theory.order_of_elementgroup_theory.p_groupgroup_theory.perm.cycle.basicgroup_theory.perm.cycle.concretegroup_theory.perm.cycle.typegroup_theory.perm.fingroup_theory.perm.optiongroup_theory.perm.signgroup_theory.schreiergroup_theory.schur_zassenhausgroup_theory.solvablegroup_theory.specific_groups.alternatinggroup_theory.specific_groups.cyclicgroup_theory.specific_groups.dihedralgroup_theory.specific_groups.quaterniongroup_theory.sylowgroup_theory.torsiongroup_theory.transferinformation_theory.hamminglinear_algebra.adic_completionlinear_algebra.affine_space.affine_equivlinear_algebra.affine_space.affine_maplinear_algebra.affine_space.affine_subspacelinear_algebra.affine_space.basislinear_algebra.affine_space.combinationlinear_algebra.affine_space.finite_dimensionallinear_algebra.affine_space.independentlinear_algebra.affine_space.matrixlinear_algebra.affine_space.midpointlinear_algebra.affine_space.orderedlinear_algebra.affine_space.pointwiselinear_algebra.affine_space.restrictlinear_algebra.affine_space.slopelinear_algebra.alternatinglinear_algebra.annihilating_polynomiallinear_algebra.basislinear_algebra.bilinear_formlinear_algebra.bilinear_maplinear_algebra.charpoly.basiclinear_algebra.charpoly.to_matrixlinear_algebra.clifford_algebra.basiclinear_algebra.clifford_algebra.conjugationlinear_algebra.clifford_algebra.contractionlinear_algebra.clifford_algebra.equivslinear_algebra.clifford_algebra.evenlinear_algebra.clifford_algebra.even_equivlinear_algebra.clifford_algebra.foldlinear_algebra.clifford_algebra.gradinglinear_algebra.clifford_algebra.starlinear_algebra.coevaluationlinear_algebra.contractionlinear_algebra.cross_productlinear_algebra.determinantlinear_algebra.dfinsupplinear_algebra.dimensionlinear_algebra.direct_sum.finsupplinear_algebra.direct_sum.tensor_productlinear_algebra.duallinear_algebra.exterior_algebra.basiclinear_algebra.exterior_algebra.gradinglinear_algebra.exterior_algebra.of_alternatinglinear_algebra.finite_dimensionallinear_algebra.finranklinear_algebra.finsupplinear_algebra.finsupp_vector_spacelinear_algebra.free_algebralinear_algebra.free_module.basiclinear_algebra.free_module.determinantlinear_algebra.free_module.finite.basiclinear_algebra.free_module.finite.matrixlinear_algebra.free_module.finite.ranklinear_algebra.free_module.ideal_quotientlinear_algebra.free_module.pidlinear_algebra.free_module.ranklinear_algebra.free_module.strong_rank_conditionlinear_algebra.invariant_basis_numberlinear_algebra.isomorphismslinear_algebra.lagrangelinear_algebra.linear_independentlinear_algebra.linear_pmaplinear_algebra.matrix.absolute_valuelinear_algebra.matrix.adjugatelinear_algebra.matrix.basislinear_algebra.matrix.bilinear_formlinear_algebra.matrix.blocklinear_algebra.matrix.charpoly.basiclinear_algebra.matrix.charpoly.coefflinear_algebra.matrix.charpoly.finite_fieldlinear_algebra.matrix.charpoly.linear_maplinear_algebra.matrix.charpoly.minpolylinear_algebra.matrix.circulantlinear_algebra.matrix.determinantlinear_algebra.matrix.diagonallinear_algebra.matrix.dot_productlinear_algebra.matrix.duallinear_algebra.matrix.finite_dimensionallinear_algebra.matrix.general_linear_grouplinear_algebra.matrix.hermitianlinear_algebra.matrix.invariant_basis_numberlinear_algebra.matrix.is_diaglinear_algebra.matrix.ldllinear_algebra.matrix.mv_polynomiallinear_algebra.matrix.nondegeneratelinear_algebra.matrix.nonsingular_inverselinear_algebra.matrix.orthogonallinear_algebra.matrix.polynomiallinear_algebra.matrix.pos_deflinear_algebra.matrix.reindexlinear_algebra.matrix.schur_complementlinear_algebra.matrix.sesquilinear_formlinear_algebra.matrix.special_linear_grouplinear_algebra.matrix.spectrumlinear_algebra.matrix.symmetriclinear_algebra.matrix.to_linlinear_algebra.matrix.to_linear_equivlinear_algebra.matrix.tracelinear_algebra.matrix.transvectionlinear_algebra.matrix.zpowlinear_algebra.multilinear.basiclinear_algebra.multilinear.basislinear_algebra.multilinear.finite_dimensionallinear_algebra.multilinear.tensor_productlinear_algebra.orientationlinear_algebra.pilinear_algebra.pi_tensor_productlinear_algebra.prodlinear_algebra.projectionlinear_algebra.projective_space.basiclinear_algebra.projective_space.independencelinear_algebra.projective_space.subspacelinear_algebra.quadratic_form.basiclinear_algebra.quadratic_form.complexlinear_algebra.quadratic_form.isometrylinear_algebra.quadratic_form.prodlinear_algebra.quadratic_form.reallinear_algebra.quotientlinear_algebra.quotient_pilinear_algebra.raylinear_algebra.sesquilinear_formlinear_algebra.smodeqlinear_algebra.spanlinear_algebra.std_basislinear_algebra.symplectic_grouplinear_algebra.tensor_algebra.basiclinear_algebra.tensor_algebra.gradinglinear_algebra.tensor_powerlinear_algebra.tensor_productlinear_algebra.tensor_product_basislinear_algebra.tracelinear_algebra.unitary_grouplinear_algebra.vandermondelogic.equiv.arraylogic.equiv.fintypelogic.equiv.functorlogic.equiv.transfer_instancelogic.hydrameasure_theory.card_measurable_spacemeasure_theory.category.Measmeasure_theory.constructions.pimeasure_theory.constructions.polishmeasure_theory.covering.besicovitchmeasure_theory.covering.besicovitch_vector_spacemeasure_theory.covering.density_theoremmeasure_theory.covering.differentiationmeasure_theory.covering.liminf_limsupmeasure_theory.covering.one_dimmeasure_theory.covering.vitalimeasure_theory.covering.vitali_familymeasure_theory.decomposition.jordanmeasure_theory.decomposition.lebesguemeasure_theory.decomposition.radon_nikodymmeasure_theory.decomposition.signed_hahnmeasure_theory.decomposition.unsigned_hahnmeasure_theory.function.ae_eq_funmeasure_theory.function.ae_eq_of_integralmeasure_theory.function.ae_measurable_ordermeasure_theory.function.ae_measurable_sequencemeasure_theory.function.conditional_expectation.basicmeasure_theory.function.conditional_expectation.indicatormeasure_theory.function.conditional_expectation.realmeasure_theory.function.continuous_map_densemeasure_theory.function.convergence_in_measuremeasure_theory.function.egorovmeasure_theory.function.ess_supmeasure_theory.function.floormeasure_theory.function.jacobianmeasure_theory.function.l1_spacemeasure_theory.function.l2_spacemeasure_theory.function.locally_integrablemeasure_theory.function.lp_ordermeasure_theory.function.lp_spacemeasure_theory.function.simple_func_densemeasure_theory.function.simple_func_dense_lpmeasure_theory.function.special_functions.arctanmeasure_theory.function.special_functions.basicmeasure_theory.function.special_functions.innermeasure_theory.function.strongly_measurable.basicmeasure_theory.function.strongly_measurable.innermeasure_theory.function.strongly_measurable.lpmeasure_theory.function.uniform_integrablemeasure_theory.group.actionmeasure_theory.group.add_circlemeasure_theory.group.arithmeticmeasure_theory.group.fundamental_domainmeasure_theory.group.integrationmeasure_theory.group.measurable_equivmeasure_theory.group.measuremeasure_theory.group.pointwisemeasure_theory.group.prodmeasure_theory.integral.averagemeasure_theory.integral.bochnermeasure_theory.integral.circle_integralmeasure_theory.integral.circle_transformmeasure_theory.integral.divergence_theoremmeasure_theory.integral.exp_decaymeasure_theory.integral.integrable_onmeasure_theory.integral.integral_eq_impropermeasure_theory.integral.interval_averagemeasure_theory.integral.interval_integralmeasure_theory.integral.layercakemeasure_theory.integral.lebesguemeasure_theory.integral.mean_inequalitiesmeasure_theory.integral.peak_functionmeasure_theory.integral.periodicmeasure_theory.integral.riesz_markov_kakutanimeasure_theory.integral.set_integralmeasure_theory.integral.set_to_l1measure_theory.integral.torus_integralmeasure_theory.integral.vitali_caratheodorymeasure_theory.latticemeasure_theory.measure.ae_disjointmeasure_theory.measure.ae_measurablemeasure_theory.measure.complexmeasure_theory.measure.contentmeasure_theory.measure.doublingmeasure_theory.measure.finite_measuremeasure_theory.measure.giry_monadmeasure_theory.measure.hausdorffmeasure_theory.measure.measure_spacemeasure_theory.measure.measure_space_defmeasure_theory.measure.mutually_singularmeasure_theory.measure.null_measurablemeasure_theory.measure.open_posmeasure_theory.measure.outer_measuremeasure_theory.measure.portmanteaumeasure_theory.measure.probability_measuremeasure_theory.measure.regularmeasure_theory.measure.stieltjesmeasure_theory.measure.submeasure_theory.measure.vector_measuremeasure_theory.measure.with_density_vector_measuremeasure_theory.tacticmodel_theory.basicmodel_theory.bundledmodel_theory.definabilitymodel_theory.direct_limitmodel_theory.elementary_mapsmodel_theory.encodingmodel_theory.finitely_generatedmodel_theory.fraissemodel_theory.graphmodel_theory.language_mapmodel_theory.ordermodel_theory.quotientsmodel_theory.satisfiabilitymodel_theory.semanticsmodel_theory.skolemmodel_theory.substructuresmodel_theory.syntaxmodel_theory.typesmodel_theory.ultraproductsnumber_theory.ADE_inequalitynumber_theory.arithmetic_functionnumber_theory.basicnumber_theory.bernoullinumber_theory.bernoulli_polynomialsnumber_theory.bertrandnumber_theory.class_number.admissible_absnumber_theory.class_number.admissible_card_pow_degreenumber_theory.class_number.finitenumber_theory.class_number.function_fieldnumber_theory.cyclotomic.basicnumber_theory.cyclotomic.discriminantnumber_theory.cyclotomic.galnumber_theory.cyclotomic.primitive_rootsnumber_theory.cyclotomic.ratnumber_theory.diophnumber_theory.diophantine_approximationnumber_theory.fermat4number_theory.fermat_pspnumber_theory.function_fieldnumber_theory.kummer_dedekindnumber_theory.l_seriesnumber_theory.legendre_symbol.add_characternumber_theory.legendre_symbol.gauss_eisenstein_lemmasnumber_theory.legendre_symbol.gauss_sumnumber_theory.legendre_symbol.jacobi_symbolnumber_theory.legendre_symbol.mul_characternumber_theory.legendre_symbol.norm_numnumber_theory.legendre_symbol.quadratic_reciprocitynumber_theory.legendre_symbol.zmod_charnumber_theory.liouville.basicnumber_theory.liouville.liouville_withnumber_theory.liouville.measurenumber_theory.liouville.residualnumber_theory.lucas_lehmernumber_theory.lucas_primalitynumber_theory.modularnumber_theory.modular_forms.basicnumber_theory.modular_forms.congruence_subgroupsnumber_theory.modular_forms.slash_actionsnumber_theory.modular_forms.slash_invariant_formsnumber_theory.multiplicitynumber_theory.number_field.basicnumber_theory.number_field.class_numbernumber_theory.number_field.embeddingsnumber_theory.number_field.normnumber_theory.padics.henselnumber_theory.padics.padic_integersnumber_theory.padics.padic_normnumber_theory.padics.padic_numbersnumber_theory.padics.padic_valnumber_theory.padics.ring_homsnumber_theory.pellnumber_theory.prime_countingnumber_theory.primes_congruent_onenumber_theory.pythagorean_triplesnumber_theory.ramification_inertianumber_theory.sum_four_squaresnumber_theory.sum_two_squaresnumber_theory.von_mangoldtnumber_theory.well_approximablenumber_theory.wilsonnumber_theory.zeta_valuesnumber_theory.zsqrtd.basicnumber_theory.zsqrtd.gaussian_intnumber_theory.zsqrtd.to_realorder.category.BoolAlgorder.category.FinBoolAlgorder.category.HeytAlgorder.category.NonemptyFinLinOrdorder.category.omega_complete_partial_orderorder.extension.wellorder.filter.ennrealorder.filter.filter_productorder.filter.germorder.filter.zero_and_bounded_at_filterorder.heightorder.intervalorder.jordan_holderorder.pfilterorder.prime_idealprobability.borel_cantelliprobability.cond_countprobability.conditional_expectationprobability.conditional_probabilityprobability.densityprobability.ident_distribprobability.integrationprobability.kernel.basicprobability.martingale.basicprobability.martingale.borel_cantelliprobability.martingale.centeringprobability.martingale.convergenceprobability.martingale.optional_stoppingprobability.martingale.upcrossingprobability.momentsprobability.notationprobability.probability_mass_function.basicprobability.probability_mass_function.constructionsprobability.probability_mass_function.monadprobability.probability_mass_function.uniformprobability.process.adaptedprobability.process.filtrationprobability.process.hitting_timeprobability.process.stoppingprobability.strong_lawprobability.variancerepresentation_theory.Actionrepresentation_theory.Reprepresentation_theory.basicrepresentation_theory.characterrepresentation_theory.fdReprepresentation_theory.invariantsrepresentation_theory.maschkering_theory.adjoin.basicring_theory.adjoin.fgring_theory.adjoin.fieldring_theory.adjoin.power_basisring_theory.adjoin.towerring_theory.adjoin_rootring_theory.algebra_towerring_theory.algebraicring_theory.algebraic_independentring_theory.artinianring_theory.bezoutring_theory.chain_of_divisorsring_theory.class_groupring_theory.coprime.idealring_theory.dedekind_domain.S_integerring_theory.dedekind_domain.adic_valuationring_theory.dedekind_domain.basicring_theory.dedekind_domain.dvrring_theory.dedekind_domain.factorizationring_theory.dedekind_domain.idealring_theory.dedekind_domain.integral_closurering_theory.dedekind_domain.pidring_theory.dedekind_domain.selmer_groupring_theory.discriminantring_theory.eisenstein_criterionring_theory.etalering_theory.euclidean_domainring_theory.filtrationring_theory.finite_presentationring_theory.finite_typering_theory.finitenessring_theory.flatring_theory.fractional_idealring_theory.free_comm_ringring_theory.free_ringring_theory.graded_algebra.basicring_theory.graded_algebra.homogeneous_idealring_theory.graded_algebra.homogeneous_localizationring_theory.graded_algebra.radicalring_theory.hahn_seriesring_theory.henselianring_theory.ideal.associated_primering_theory.ideal.basicring_theory.ideal.cotangentring_theory.ideal.idempotent_fgring_theory.ideal.local_ringring_theory.ideal.minimal_primering_theory.ideal.normring_theory.ideal.operationsring_theory.ideal.overring_theory.ideal.prodring_theory.ideal.quotientring_theory.int.basicring_theory.integral_closurering_theory.integral_domainring_theory.integrally_closedring_theory.is_adjoin_rootring_theory.is_tensor_productring_theory.jacobsonring_theory.jacobson_idealring_theory.laurent_seriesring_theory.local_propertiesring_theory.localization.as_subringring_theory.localization.at_primering_theory.localization.basicring_theory.localization.cardinalityring_theory.localization.fraction_ringring_theory.localization.idealring_theory.localization.integerring_theory.localization.integralring_theory.localization.inv_submonoidring_theory.localization.localization_localizationring_theory.localization.modulering_theory.localization.normring_theory.localization.num_denomring_theory.localization.submodulering_theory.matrix_algebraring_theory.multiplicityring_theory.mv_polynomial.basicring_theory.mv_polynomial.homogeneousring_theory.mv_polynomial.symmetricring_theory.mv_polynomial.towerring_theory.nakayamaring_theory.nilpotentring_theory.noetherianring_theory.non_unital_subsemiring.basicring_theory.normring_theory.nullstellensatzring_theory.perfectionring_theory.polynomial.basicring_theory.polynomial.bernsteinring_theory.polynomial.chebyshevring_theory.polynomial.contentring_theory.polynomial.cyclotomic.basicring_theory.polynomial.cyclotomic.evalring_theory.polynomial.dicksonring_theory.polynomial.eisenstein.basicring_theory.polynomial.eisenstein.is_integralring_theory.polynomial.gauss_lemmaring_theory.polynomial.oppositesring_theory.polynomial.pochhammerring_theory.polynomial.rational_rootring_theory.polynomial.scale_rootsring_theory.polynomial.selmerring_theory.polynomial.towerring_theory.polynomial.vietaring_theory.polynomial_algebraring_theory.power_basisring_theory.power_series.basicring_theory.power_series.well_knownring_theory.principal_ideal_domainring_theory.rees_algebraring_theory.ring_hom.finitering_theory.ring_hom.finite_typering_theory.ring_hom.integralring_theory.ring_hom.surjectivering_theory.ring_hom_propertiesring_theory.simple_modulering_theory.subring.pointwisering_theory.tensor_productring_theory.tracering_theory.unique_factorization_domainring_theory.valuation.basicring_theory.valuation.extend_to_localizationring_theory.valuation.integersring_theory.valuation.integralring_theory.valuation.ramification_groupring_theory.valuation.valuation_ringring_theory.valuation.valuation_subringring_theory.witt_vector.basicring_theory.witt_vector.comparering_theory.witt_vector.defsring_theory.witt_vector.discrete_valuation_ringring_theory.witt_vector.domainring_theory.witt_vector.frobeniusring_theory.witt_vector.frobenius_fraction_fieldring_theory.witt_vector.identitiesring_theory.witt_vector.init_tailring_theory.witt_vector.is_polyring_theory.witt_vector.isocrystalring_theory.witt_vector.mul_coeffring_theory.witt_vector.mul_pring_theory.witt_vector.structure_polynomialring_theory.witt_vector.teichmullerring_theory.witt_vector.truncatedring_theory.witt_vector.verschiebungring_theory.witt_vector.witt_polynomialset_theory.cardinal.cofinalityset_theory.cardinal.continuumset_theory.cardinal.divisibilityset_theory.cardinal.ordinalset_theory.game.basicset_theory.game.birthdayset_theory.game.domineeringset_theory.game.impartialset_theory.game.nimset_theory.game.ordinalset_theory.game.pgameset_theory.game.shortset_theory.game.stateset_theory.ordinal.arithmeticset_theory.ordinal.cantor_normal_formset_theory.ordinal.fixed_pointset_theory.ordinal.natural_opsset_theory.ordinal.notationset_theory.ordinal.principalset_theory.ordinal.topologyset_theory.surreal.basicset_theory.surreal.dyadicset_theory.zfc.basicset_theory.zfc.ordinaltactic.grouptesting.slim_check.functionstesting.slim_check.gentesting.slim_check.sampleabletesting.slim_check.testabletopology.algebra.affinetopology.algebra.algebratopology.algebra.continuous_affine_maptopology.algebra.continuous_monoid_homtopology.algebra.equicontinuitytopology.algebra.fieldtopology.algebra.filter_basistopology.algebra.group.basictopology.algebra.group.compacttopology.algebra.group_completiontopology.algebra.group_with_zerotopology.algebra.localizationtopology.algebra.module.basictopology.algebra.module.character_spacetopology.algebra.module.determinanttopology.algebra.module.finite_dimensiontopology.algebra.module.linear_pmaptopology.algebra.module.locally_convextopology.algebra.module.multilineartopology.algebra.module.strong_topologytopology.algebra.module.weak_dualtopology.algebra.monoidtopology.algebra.nonarchimedean.adic_topologytopology.algebra.nonarchimedean.basestopology.algebra.nonarchimedean.basictopology.algebra.open_subgrouptopology.algebra.order.fieldtopology.algebra.order.floortopology.algebra.order.grouptopology.algebra.polynomialtopology.algebra.star_subalgebratopology.algebra.uniform_convergencetopology.algebra.uniform_fieldtopology.algebra.uniform_filter_basistopology.algebra.uniform_grouptopology.algebra.uniform_mul_actiontopology.algebra.uniform_ringtopology.algebra.valuationtopology.algebra.valued_fieldtopology.algebra.with_zero_topologytopology.category.Borntopology.category.CompHaus.basictopology.category.CompHaus.projectivetopology.category.Compactumtopology.category.Localetopology.category.Profinite.as_limittopology.category.Profinite.basictopology.category.Profinite.cofiltered_limittopology.category.Profinite.projectivetopology.category.Top.adjunctionstopology.category.Top.basictopology.category.Top.epi_monotopology.category.Top.open_nhdstopology.category.Top.openstopology.category.TopCommRingtopology.category.UniformSpacetopology.continuous_function.algebratopology.continuous_function.boundedtopology.continuous_function.compacttopology.continuous_function.idealstopology.continuous_function.locally_constanttopology.continuous_function.orderedtopology.continuous_function.polynomialtopology.continuous_function.stone_weierstrasstopology.continuous_function.unitstopology.continuous_function.weierstrasstopology.continuous_function.zero_at_inftytopology.coveringtopology.fiber_bundle.basictopology.fiber_bundle.constructionstopology.fiber_bundle.trivializationtopology.gluingtopology.homotopy.basictopology.homotopy.contractibletopology.homotopy.equivtopology.homotopy.homotopy_grouptopology.homotopy.pathtopology.homotopy.producttopology.instances.add_circletopology.instances.complextopology.instances.discretetopology.instances.ennrealtopology.instances.erealtopology.instances.inttopology.instances.irrationaltopology.instances.matrixtopology.instances.nattopology.instances.nnrealtopology.instances.rattopology.instances.rat_lemmastopology.instances.realtopology.instances.real_vector_spacetopology.instances.triv_sq_zero_exttopology.is_locally_homeomorphtopology.listtopology.local_at_targettopology.local_homeomorphtopology.locally_constant.algebratopology.metric_space.algebratopology.metric_space.antilipschitztopology.metric_space.bairetopology.metric_space.basictopology.metric_space.cau_seq_filtertopology.metric_space.closedstopology.metric_space.completiontopology.metric_space.contractingtopology.metric_space.emetric_paracompacttopology.metric_space.emetric_spacetopology.metric_space.equicontinuitytopology.metric_space.gluingtopology.metric_space.gromov_hausdorfftopology.metric_space.gromov_hausdorff_realizedtopology.metric_space.hausdorff_dimensiontopology.metric_space.hausdorff_distancetopology.metric_space.holdertopology.metric_space.infseptopology.metric_space.isometric_smultopology.metric_space.isometrytopology.metric_space.kuratowskitopology.metric_space.lipschitztopology.metric_space.metric_separatedtopology.metric_space.metrizabletopology.metric_space.metrizable_uniformitytopology.metric_space.partition_of_unitytopology.metric_space.pi_nattopology.metric_space.polishtopology.metric_space.shrinking_lemmatopology.metric_space.thickened_indicatortopology.order.hom.esakiatopology.partition_of_unitytopology.path_connectedtopology.semicontinuoustopology.sequencestopology.sets.compactstopology.sheaves.abeliantopology.sheaves.forgettopology.sheaves.functorstopology.sheaves.limitstopology.sheaves.local_predicatetopology.sheaves.locally_surjectivetopology.sheaves.operationstopology.sheaves.presheaftopology.sheaves.presheaf_of_functionstopology.sheaves.punittopology.sheaves.sheaftopology.sheaves.sheaf_condition.equalizer_productstopology.sheaves.sheaf_condition.opens_le_covertopology.sheaves.sheaf_condition.pairwise_intersectionstopology.sheaves.sheaf_condition.sitestopology.sheaves.sheaf_condition.unique_gluingtopology.sheaves.sheaf_of_functionstopology.sheaves.sheafifytopology.sheaves.skyscrapertopology.sheaves.stalkstopology.tactictopology.tietze_extensiontopology.uniform_space.compacttopology.uniform_space.compact_convergencetopology.uniform_space.compare_realstopology.uniform_space.completiontopology.uniform_space.equicontinuitytopology.uniform_space.matrixtopology.uniform_space.uniform_convergence_topologytopology.unit_intervaltopology.urysohns_boundedtopology.urysohns_lemmatopology.vector_bundle.basictopology.vector_bundle.constructionstopology.vector_bundle.homThe following files have no module docstring, so I have not added a message in this PR
control.basiccontrol.monad.contcontrol.monad.writercontrol.traversable.derivedata.array.lemmasdata.bitvec.basicdata.buffer.basicdata.rbmap.basicdata.rbmap.defaultdata.rbtree.basicdata.rbtree.default_ltdata.rbtree.finddata.rbtree.initdata.rbtree.insertdata.rbtree.maindata.rbtree.min_maxdata.seq.computationdata.seq.paralleldata.seq.seqdata.seq.wseqPlease make a PR to add a module docstring (for Lean3 and Lean4!), then I will add the freeze comment next time.
The following files no longer exist in Lean 3' mathlib, so I have not added a message in this PR
algebra.category.Module.monoidal.basicalgebra.category.Module.monoidal.closedalgebra.category.Module.monoidal.symmetricalgebra.dual_quaternionalgebra.expralgebra.field.uliftalgebra.homology.local_cohomologyalgebra.modeqalgebra.module.zlatticealgebra.monoid_algebra.divisionalgebra.monoid_algebra.idealalgebra.order.nonneg.flooralgebra.star.orderalgebraic_geometry.open_immersion.Schemealgebraic_geometry.open_immersion.basicalgebraic_topology.dold_kan.compatibilityalgebraic_topology.dold_kan.equivalencealgebraic_topology.dold_kan.equivalence_pseudoabeliananalysis.calculus.cont_diff_defanalysis.calculus.deriv.addanalysis.calculus.deriv.basicanalysis.calculus.deriv.companalysis.calculus.deriv.invanalysis.calculus.deriv.inverseanalysis.calculus.deriv.linearanalysis.calculus.deriv.mulanalysis.calculus.deriv.polynomialanalysis.calculus.deriv.powanalysis.calculus.deriv.prodanalysis.calculus.deriv.slopeanalysis.calculus.deriv.staranalysis.calculus.deriv.supportanalysis.calculus.deriv.zpowanalysis.calculus.fderiv.addanalysis.calculus.fderiv.basicanalysis.calculus.fderiv.bilinearanalysis.calculus.fderiv.companalysis.calculus.fderiv.equivanalysis.calculus.fderiv.linearanalysis.calculus.fderiv.mulanalysis.calculus.fderiv.prodanalysis.calculus.fderiv.restrict_scalarsanalysis.calculus.fderiv.staranalysis.complex.upper_half_plane.manifoldanalysis.convex.cone.dualanalysis.convex.cone.properanalysis.convex.specific_functions.basicanalysis.convex.specific_functions.derivanalysis.fourier.fourier_transformanalysis.fourier.poisson_summationanalysis.inner_product_space.linear_pmapanalysis.inner_product_space.of_normanalysis.inner_product_space.orthogonalanalysis.locally_convex.strong_topologyanalysis.mellin_transformanalysis.normed.mul_actionanalysis.normed.order.upper_loweranalysis.normed_space.quaternion_exponentialanalysis.normed_space.star.continuous_functional_calculusanalysis.normed_space.star.multiplieranalysis.special_functions.gamma.basicanalysis.special_functions.gamma.betaanalysis.special_functions.gamma.bohr_mollerupanalysis.special_functions.improper_integralsanalysis.special_functions.pow.asymptoticsanalysis.special_functions.pow.complexanalysis.special_functions.pow.continuityanalysis.special_functions.pow.derivanalysis.special_functions.pow.nnrealanalysis.special_functions.pow.realarithcccanonically_ordered_comm_semiring_two_mulcategory_theory.cofiltered_systemcategory_theory.limits.constructions.over.basiccategory_theory.monoidal.Mod_category_theory.monoidal.of_chosen_finite_products.basiccategory_theory.monoidal.of_chosen_finite_products.symmetriccategory_theory.monoidal.types.basiccategory_theory.monoidal.types.coyonedacategory_theory.monoidal.types.symmetriccategory_theory.preadditive.yoneda.basiccategory_theory.preadditive.yoneda.injectivecategory_theory.preadditive.yoneda.limitscategory_theory.preadditive.yoneda.projectivecategory_theory.shift.basiccategory_theory.sites.pushforwardchar_p_zero_ne_char_zerocombinatorics.additive.e_transformcombinatorics.quiver.coveringcombinatorics.simple_graph.finsubgraphcombinatorics.simple_graph.regularity.chunkcombinatorics.simple_graph.regularity.incrementcombinatorics.simple_graph.regularity.lemmacyclotomic_105data.buffer.parserdata.complex.orientationdata.dlistdata.fin.tuple.reflectiondata.list.to_finsuppdata.matrix.autodata.matrix.dual_numberdata.matrix.invertibledata.matrix.reflectiondata.mv_polynomial.divisiondata.mv_polynomial.polynomialdata.nat.factorial.double_factorialdata.rat.stardata.set.listdata.set.ncarddata.set.pairwise.basicdata.set.pairwise.latticedata.set.supsdata.vectordirect_sum_is_internalexamples.mersenne_primesexamples.prop_encodablefield_theory.ax_grothendieckfield_theory.is_alg_closed.spectrumfield_theory.splitting_field.constructionfield_theory.splitting_field.is_splitting_fieldgeometry.euclidean.sphere.basicgeometry.euclidean.sphere.powergeometry.euclidean.sphere.ptolemygeometry.euclidean.sphere.second_intergeometry.manifold.sheaf.basicgeometry.manifold.vector_bundle.basicgeometry.manifold.vector_bundle.fiberwise_lineargeometry.manifold.vector_bundle.homgeometry.manifold.vector_bundle.pullbackgeometry.manifold.vector_bundle.smooth_sectiongeometry.manifold.vector_bundle.tangentgirardhomogeneous_prime_not_primeimo.imo1959_q1imo.imo1960_q1imo.imo1962_q1imo.imo1962_q4imo.imo1964_q1imo.imo1969_q1imo.imo1972_q5imo.imo1975_q1imo.imo1977_q6imo.imo1981_q3imo.imo1987_q1imo.imo1988_q6imo.imo1994_q1imo.imo1998_q2imo.imo2001_q2imo.imo2001_q6imo.imo2005_q3imo.imo2005_q4imo.imo2006_q3imo.imo2006_q5imo.imo2008_q2imo.imo2008_q3imo.imo2008_q4imo.imo2011_q3imo.imo2011_q5imo.imo2013_q1imo.imo2013_q5imo.imo2019_q1imo.imo2019_q2imo.imo2019_q4imo.imo2020_q2imo.imo2021_q1init.algebra.classesinit.algebra.functionsinit.algebra.orderinit.control.lawfulinit.data.int.bitwiseinit.data.int.comp_lemmasinit.data.list.instancesinit.data.list.lemmasinit.data.nat.bitwiseinit.data.nat.gcdinit.data.nat.lemmasinit.data.ordering.lemmasinit.data.sigma.lexinit.data.subtype.basicinit.functioninit.ite_simpinit.meta.well_founded_tacticslinear_algebra.affine_space.midpoint_zerolinear_algebra.basis.bilinearlinear_algebra.bilinear_form.tensor_productlinear_algebra.eigenspace.basiclinear_algebra.eigenspace.is_alg_closedlinear_algebra.eigenspace.minpolylinear_algebra.free_module.normlinear_algebra.matrix.charpoly.eigslinear_algebra.quadratic_form.duallinear_algebra.tensor_algebra.to_tensor_powerlinear_algebra.tensor_product.matrixlinear_order_with_pos_mul_pos_eq_zeromap_floormeasure_theory.constructions.borel_space.basicmeasure_theory.constructions.borel_space.complexmeasure_theory.constructions.borel_space.continuous_linear_mapmeasure_theory.constructions.borel_space.metrizablemeasure_theory.constructions.prod.basicmeasure_theory.constructions.prod.integralmeasure_theory.function.conditional_expectation.ae_measurablemeasure_theory.function.conditional_expectation.condexp_L1measure_theory.function.conditional_expectation.condexp_L2measure_theory.function.conditional_expectation.uniquemeasure_theory.function.lp_seminormmeasure_theory.function.simple_funcmeasure_theory.function.special_functions.is_R_or_Cmeasure_theory.group.geometry_of_numbersmeasure_theory.integral.fund_thm_calculusmeasure_theory.integral.lebesgue_normed_spacemeasure_theory.measure.haar.basicmeasure_theory.measure.haar.inner_product_spacemeasure_theory.measure.haar.normed_spacemeasure_theory.measure.haar.of_basismeasure_theory.measure.haar.quotientmeasure_theory.measure.lebesgue.basicmeasure_theory.measure.lebesgue.complexmeasure_theory.measure.lebesgue.eq_haarmeasure_theory.measure.lebesgue.integralmiu_language.basicmiu_language.decision_necmiu_language.decision_sufnumber_theory.legendre_symbol.basicnumber_theory.legendre_symbol.quadratic_char.basicnumber_theory.legendre_symbol.quadratic_char.gauss_sumnumber_theory.liouville.liouville_numbernumber_theory.modular_forms.jacobi_theta.basicnumber_theory.modular_forms.jacobi_theta.manifoldnumber_theory.number_field.canonical_embeddingnumber_theory.number_field.unitsnumber_theory.pell_matiyasevicnumber_theory.zeta_functionnumber_theory.zsqrtd.quadratic_reciprocityorder.category.BddDistLatorder.category.BddLatorder.category.BddOrdorder.category.CompleteLatorder.category.DistLatorder.category.FinBddDistLatorder.category.FinPartOrdorder.category.Frmorder.category.Latorder.category.LinOrdorder.category.PartOrdorder.category.Preordorder.category.Semilatorder.irreducibleorder.upper_lower.locally_finiteoxford_invariants.«2021summer».week3_p1phillipsprobability.independence.basicprobability.independence.zero_oneprobability.kernel.compositionprobability.kernel.cond_cdfprobability.kernel.cond_distribprobability.kernel.condexpprobability.kernel.disintegrationprobability.kernel.integral_comp_prodprobability.kernel.invarianceprobability.kernel.measurable_integralprobability.kernel.with_densityprobability.martingale.optional_samplingpseudoelementquadratic_formrepresentation_theory.group_cohomology.basicrepresentation_theory.group_cohomology.resolutionring_theory.complexring_theory.dedekind_domain.finite_adele_ringring_theory.derivation.basicring_theory.derivation.liering_theory.derivation.to_square_zeroring_theory.discrete_valuation_ring.basicring_theory.discrete_valuation_ring.tfaering_theory.ideal.quotient_operationsring_theory.kaehlerring_theory.localization.away.adjoin_rootring_theory.localization.away.basicring_theory.mv_polynomial.idealring_theory.mv_polynomial.weighted_homogeneousring_theory.polynomial.cyclotomic.expandring_theory.polynomial.cyclotomic.rootsring_theory.polynomial.hermite.basicring_theory.polynomial.hermite.gaussianring_theory.polynomial.quotientring_theory.quotient_nilpotentring_theory.quotient_noetherianring_theory.roots_of_unity.basicring_theory.roots_of_unity.complexring_theory.roots_of_unity.minpolyring_theory.valuation.quotientring_theory.zmodseminorm_lattice_not_distribsensitivityset_theory.ordinal.exponentialsorgenfrey_linetopology.algebra.infinite_sum.basictopology.algebra.infinite_sum.moduletopology.algebra.infinite_sum.ordertopology.algebra.infinite_sum.realtopology.algebra.infinite_sum.ringtopology.algebra.module.simpletopology.algebra.module.startopology.algebra.order.upper_lowertopology.algebra.ring.basictopology.algebra.ring.idealtopology.category.Top.limits.basictopology.category.Top.limits.cofilteredtopology.category.Top.limits.konigtopology.category.Top.limits.productstopology.category.Top.limits.pullbackstopology.extremally_disconnectedtopology.homotopy.H_spacestopology.metric_space.cantor_schemetopology.metric_space.dilationwiedijk_100_theorems.abel_ruffiniwiedijk_100_theorems.area_of_a_circlewiedijk_100_theorems.ascending_descending_sequenceswiedijk_100_theorems.ballot_problemwiedijk_100_theorems.birthday_problemwiedijk_100_theorems.cubing_a_cubewiedijk_100_theorems.friendship_graphswiedijk_100_theorems.herons_formulawiedijk_100_theorems.inverse_triangle_sumwiedijk_100_theorems.konigsbergwiedijk_100_theorems.partitionwiedijk_100_theorems.perfect_numberswiedijk_100_theorems.solution_of_cubicwiedijk_100_theorems.sum_of_prime_reciprocals_divergeszero_divisors_in_add_monoid_algebrasIn future we should find where they moved to, and check that the files are still in sync.
I am a bot; please check that I have not put a comment in a bad place before running
bors merge!