mathlib
9240e8be - chore(*): add mathlib4 synchronization comments (#19218)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19218) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebraic_geometry.elliptic_curve.weierstrass` * `analysis.complex.upper_half_plane.basic` * `analysis.complex.upper_half_plane.functions_bounded_at_infty` * `analysis.complex.upper_half_plane.metric` * `analysis.complex.upper_half_plane.topology` * `analysis.fourier.riemann_lebesgue_lemma` * `analysis.inner_product_space.linear_pmap` * `analysis.special_functions.gamma.beta` * `category_theory.closed.ideal` * `category_theory.monad.equiv_mon` * `control.random` * `geometry.euclidean.monge_point` * `geometry.manifold.complex` * `geometry.manifold.partition_of_unity` * `logic.equiv.array` * `number_theory.legendre_symbol.jacobi_symbol` * `number_theory.modular` * `number_theory.modular_forms.jacobi_theta.basic` * `number_theory.modular_forms.slash_actions` * `number_theory.modular_forms.slash_invariant_forms` * `ring_theory.witt_vector.compare` * `ring_theory.witt_vector.discrete_valuation_ring` * `ring_theory.witt_vector.domain` * `ring_theory.witt_vector.frobenius` * `ring_theory.witt_vector.identities` * `ring_theory.witt_vector.init_tail` * `ring_theory.witt_vector.mul_coeff` * `ring_theory.witt_vector.truncated` * `ring_theory.witt_vector.verschiebung` * `set_theory.game.birthday` * `set_theory.game.impartial` * `set_theory.surreal.basic` * `testing.slim_check.gen` * `testing.slim_check.sampleable` * `testing.slim_check.testable`
Parents
Loading