RemyDegenne
commented
1 year ago bors r+
Closed github-actions[bot] closed 1 year ago
RemyDegenne
commented
1 year ago bors r+
bors[bot]
commented
1 year ago Pull request successfully merged into master.
Build succeeded!
The publicly hosted instance of bors-ng is deprecated and will go away soon.
If you want to self-host your own instance, instructions are here. For more help, visit the forum.
If you want to switch to GitHub's built-in merge queue, visit their help page.
Regenerated from the port status wiki page. Relates to the following files:
algebra.category.Mon.colimitsalgebra.category.fgModule.basicanalysis.complex.upper_half_plane.basicanalysis.inner_product_space.linear_pmapanalysis.special_functions.gamma.betaanalysis.special_functions.gamma.bohr_mollerupanalysis.special_functions.gaussiancategory_theory.closed.idealcategory_theory.monoidal.Bimodcombinatorics.simple_graph.regularity.boundcombinatorics.simple_graph.regularity.chunkcombinatorics.simple_graph.regularity.incrementcombinatorics.simple_graph.regularity.lemmacontrol.randomgeometry.manifold.complexgeometry.manifold.mfderivgeometry.manifold.partition_of_unitylinear_algebra.exterior_algebra.of_alternatinglogic.equiv.arraynumber_theory.bertrandnumber_theory.legendre_symbol.gauss_eisenstein_lemmasnumber_theory.legendre_symbol.gauss_sumnumber_theory.legendre_symbol.jacobi_symbolnumber_theory.legendre_symbol.quadratic_char.gauss_sumnumber_theory.legendre_symbol.quadratic_reciprocitynumber_theory.sum_two_squaresnumber_theory.zsqrtd.quadratic_reciprocityring_theory.dedekind_domain.selmer_groupring_theory.witt_vector.frobeniusring_theory.witt_vector.identitiesring_theory.witt_vector.init_tailring_theory.witt_vector.verschiebungset_theory.game.basicset_theory.game.impartialset_theory.game.ordinalset_theory.surreal.basictesting.slim_check.gentesting.slim_check.sampleabletesting.slim_check.testableThe following files have no module docstring, so I have not added a message in this PR
control.basiccontrol.monad.contcontrol.monad.writerdata.bitvec.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
canonically_ordered_comm_semiring_two_mulchar_p_zero_ne_char_zerocyclotomic_105direct_sum_is_internalexamples.prop_encodablegirardimo.imo1959_q1imo.imo1960_q1imo.imo1962_q1imo.imo1962_q4imo.imo1964_q1imo.imo1969_q1imo.imo1972_q5imo.imo1975_q1imo.imo1977_q6imo.imo1981_q3imo.imo1987_q1imo.imo1994_q1imo.imo2001_q2imo.imo2001_q6imo.imo2005_q3imo.imo2006_q3imo.imo2006_q5imo.imo2008_q3imo.imo2008_q4imo.imo2011_q3imo.imo2011_q5imo.imo2013_q1imo.imo2013_q5imo.imo2019_q1imo.imo2019_q4imo.imo2020_q2imo.imo2021_q1lean_core.data.dlistlean_core.data.vectorlinear_order_with_pos_mul_pos_eq_zeromap_floormiu_language.basicmiu_language.decision_necmiu_language.decision_sufphillipsquadratic_formseminorm_lattice_not_distribsensitivitywiedijk_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!