!3#17923

Stream: PR reviews

[Scott Morrison]

@Joël Riou, I've just hit merge on your mathlib3 PR !3#17923. It should be ready for forward porting to Mathlib4 via mathport in about 24 hours. You did so much porting that I'm sure you'll have no trouble, but please just ping here if anything goes awry, or it would be helpful to have someone else take it over.

[Joël Riou]

Thanks! The forward port PR is #6186.

[Joël Riou]

Now that #6186 is merged, I am not sure what to do with the last two Dold-Kan PRs !3#17925 and !3#17926. Should it be merged in mathlib3? or should I port them directly to mathlib4?

[Scott Morrison]

I think this is up to your preference, whatever you think will be smoothest. I just :peace_sign:'d !3#17925, if that helps!