A small repo of the proof that an abelian group is injective iff divisible. Hopefully this will expand into a repo for injective objects, and then sheaf cohomology.
generated from github/welcome-to-github
-
Notifications
You must be signed in to change notification settings - Fork 0
uzulim/lean_injective_divisible
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Producing a Lean proof that an abelian group is injective iff divisible
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published