mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: golf SpectrumRestricts.closedEmbedding_starAlgHom using uniform trickery

Open ADedecker opened this issue 1 year ago • 1 comments
trafficstars

  • [x] depends on: #13015
  • [x] depends on: #13018
  • [ ] depends on: #13019

Open in Gitpod

ADedecker avatar May 18 '24 22:05 ADedecker

This PR/issue depends on:

  • ~~leanprover-community/mathlib4#13015~~
  • ~~leanprover-community/mathlib4#13018~~
  • ~~leanprover-community/mathlib4#13019~~ By Dependent Issues (🤖). Happy coding!

leanprover-community-mathlib4-bot avatar May 23 '24 13:05 leanprover-community-mathlib4-bot

Thanks!

bors merge

j-loreaux avatar May 24 '24 22:05 j-loreaux

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar May 24 '24 22:05 mathlib-bors[bot]