Closed github-actions[bot] closed 1 year ago
bors r+
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.Algebra.basic
algebra.category.Algebra.limits
algebra.category.Module.change_of_rings
algebra.module.pid
algebraic_geometry.elliptic_curve.point
algebraic_geometry.morphisms.quasi_compact
algebraic_geometry.morphisms.quasi_separated
algebraic_geometry.projective_spectrum.structure_sheaf
algebraic_topology.fundamental_groupoid.induced_maps
algebraic_topology.fundamental_groupoid.product
algebraic_topology.fundamental_groupoid.simply_connected
analysis.normed.group.SemiNormedGroup.kernels
category_theory.adjunction.lifting
category_theory.monoidal.internal.Module
data.qpf.multivariate.constructions.cofix
geometry.manifold.diffeomorph
geometry.manifold.vector_bundle.smooth_section
geometry.manifold.whitney_embedding
group_theory.finite_abelian
linear_algebra.clifford_algebra.contraction
linear_algebra.exterior_algebra.grading
linear_algebra.matrix.schur_complement
linear_algebra.tensor_algebra.to_tensor_power
model_theory.direct_limit
model_theory.fraisse
number_theory.modular_forms.basic
representation_theory.character
representation_theory.group_cohomology.basic
ring_theory.jacobson
ring_theory.nullstellensatz
topology.metric_space.gromov_hausdorff
topology.vector_bundle.hom
The following files have no module docstring, so I have not added a message in this PR
control.basic
control.monad.cont
control.monad.writer
data.bitvec.basic
data.rbmap.basic
data.rbmap.default
data.rbtree.basic
data.rbtree.default_lt
data.rbtree.find
data.rbtree.init
data.rbtree.insert
data.rbtree.main
data.rbtree.min_max
data.seq.computation
data.seq.parallel
data.seq.seq
data.seq.wseq
Please 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
arithcc
canonically_ordered_comm_semiring_two_mul
char_p_zero_ne_char_zero
cyclotomic_105
direct_sum_is_internal
examples.mersenne_primes
examples.prop_encodable
girard
homogeneous_prime_not_prime
imo.imo1959_q1
imo.imo1960_q1
imo.imo1962_q1
imo.imo1962_q4
imo.imo1964_q1
imo.imo1969_q1
imo.imo1972_q5
imo.imo1975_q1
imo.imo1977_q6
imo.imo1981_q3
imo.imo1987_q1
imo.imo1988_q6
imo.imo1994_q1
imo.imo1998_q2
imo.imo2001_q2
imo.imo2001_q6
imo.imo2005_q3
imo.imo2006_q3
imo.imo2006_q5
imo.imo2008_q2
imo.imo2008_q3
imo.imo2008_q4
imo.imo2011_q3
imo.imo2011_q5
imo.imo2013_q1
imo.imo2013_q5
imo.imo2019_q1
imo.imo2019_q2
imo.imo2019_q4
imo.imo2020_q2
imo.imo2021_q1
lean_core.data.dlist
lean_core.data.vector
linear_order_with_pos_mul_pos_eq_zero
map_floor
miu_language.basic
miu_language.decision_nec
miu_language.decision_suf
oxford_invariants.2021summer.week3_p1
phillips
pseudoelement
quadratic_form
seminorm_lattice_not_distrib
sensitivity
sorgenfrey_line
wiedijk_100_theorems.abel_ruffini
wiedijk_100_theorems.area_of_a_circle
wiedijk_100_theorems.ascending_descending_sequences
wiedijk_100_theorems.ballot_problem
wiedijk_100_theorems.birthday_problem
wiedijk_100_theorems.cubing_a_cube
wiedijk_100_theorems.friendship_graphs
wiedijk_100_theorems.herons_formula
wiedijk_100_theorems.inverse_triangle_sum
wiedijk_100_theorems.konigsberg
wiedijk_100_theorems.partition
wiedijk_100_theorems.perfect_numbers
wiedijk_100_theorems.solution_of_cubic
wiedijk_100_theorems.sum_of_prime_reciprocals_diverges
zero_divisors_in_add_monoid_algebras
In 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
!