[Merged by Bors] - chore: fix implicit-reducible diamond in uniform convergence#38481

sgouezel wants to merge 1 commit intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

sgouezel:SG_lintUnif37sgouezel/mathlib4:SG_lintUnif37Copy head branch name to clipboard