Skip to content

Pull requests: chrisflav/proetale

New pull request New
14 Open 157 Closed
14 Open 157 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat(Algebra/WeaklyEtaleField): a weakly étale extension of fields is separable algebraic (Stacks 092P) fable
#179 opened Jun 12, 2026 by chrisflav Owner Loading…
feat(Algebra/WLocalization): close zeroLocus_ideal_eq and isWLocalRing sorries fable
#178 opened Jun 12, 2026 by chrisflav Owner Loading…
feat(Algebra/IndEtale): nontrivial idempotents in ind-étale algebras over fields fable
#177 opened Jun 12, 2026 by chrisflav Owner Loading…
feat(Algebra/Bijective): a weakly étale bijective-on-residue-fields local hom is an isomorphism fable
#170 opened Jun 12, 2026 by chrisflav Owner Loading…
feat(Algebra/IndWeaklyEtale): every ind-étale algebra is weakly étale fable
#169 opened Jun 12, 2026 by chrisflav Owner Loading…
1
TotallyDisconnected
#166 opened Jun 11, 2026 by haowen214 Contributor Loading…
2
fabel output
#165 opened Jun 10, 2026 by chrisflav Owner • Draft
feat(Mathlib/RingTheory/WeaklyEtale/GoDown): faithfully flat intermediate descent of weakly étale algebras archon Upstreamed from `archon` branch
#160 opened Jun 9, 2026 by chrisflav Owner Loading…
3 tasks done
feat(Topology/SpectralSpace/WLocal/Pullback): fill sorries for Stacks 096C (second part) archon Upstreamed from `archon` branch
#158 opened Jun 9, 2026 by chrisflav Owner Loading…
2 tasks done
chore: bump mathlib to 236391b auto-bump dependencies
#131 opened Jun 2, 2026 by github-actions Bot Loading…
feat(Algebra/WContractible): w-localness and π₀-equivalence of Restriction archon Upstreamed from `archon` branch
#130 opened Jun 2, 2026 by chrisflav Owner Loading…
2 tasks done
8
feat(Mathlib/RingTheory/LocalRing): extended maximal ideal lies in Jacobson radical for finite extensions archon Upstreamed from `archon` branch
#108 opened May 25, 2026 by chrisflav Owner Loading…
5
feat(Algebra/IndZariski): fill bijectiveOnStalks_algebraMap and of_colimitPresentation sorries archon Upstreamed from `archon` branch
#92 opened May 22, 2026 by chrisflav Owner Loading…
1 task done
26
feat(Algebra/Category/Ring/FilteredDescent): FP-algebra descent along filtered colimit (Stacks 00U3) archon Upstreamed from `archon` branch
#73 opened May 21, 2026 by chrisflav Owner Loading…
13
ProTip! What’s not been updated in a month: updated:<2026-05-16.