Skip to content

feat (Data/Equiv/Basic): add equiv#13

Merged
gebner merged 10 commits intoleanprover-community:masterfrom
kbuzzard:equiv
Jun 9, 2021
Merged

feat (Data/Equiv/Basic): add equiv#13
gebner merged 10 commits intoleanprover-community:masterfrom
kbuzzard:equiv

Conversation

@kbuzzard
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard commented Jun 3, 2021

If this is too big let me know. This was stuff I needed for a small project.

gebner
gebner reviewed Jun 3, 2021
View reviewed changes
Mathlib/Lemma.lean Outdated
@@ -0,0 +1,3 @@
-- this macro, written by Sebastian Ullrich, enables us to have lemmas
macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command => `($mods:declModifiers theorem $n $sig $val)
Copy link
Copy Markdown
Member

@gebner gebner Jun 3, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Two things:

  1. we already have this
  2. you need to add every file to Mathlib.lean now because leanpkg only builds its dependencies nowadays. @Kha Is that intentional?
  3. I can't import both Mathlib.Lemma and Mathlib.Tactic.Basic now because of the error import failed, environment already contains 'command_Lemma___._closed_6._cstage2'. Since you're already here @Kha, is this is a bug?

Copy link
Copy Markdown
Collaborator

@Kha Kha Jun 4, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you need to add every file to Mathlib.lean now because leanpkg only builds its dependencies nowadays. @Kha Is that intentional?

Yes, like in Rust (if I'm not mistaken). It does have the nice effect that stray files (e.g. from a change otherwise stashed away) don't break your build.

Copy link
Copy Markdown
Collaborator

@Kha Kha Jun 4, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can't import both Mathlib.Lemma and Mathlib.Tactic.Basic now

Sadly it seems unavoidable if we want to give parsers reasonable names (so we can open them)

Copy link
Copy Markdown
Member

@digama0 digama0 Jun 4, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Rust will follow transitive dependencies though. That would probably work better for us since we already have the default.lean files which import everything in a subdirectory.

Copy link
Copy Markdown
Member

@digama0 digama0 Jun 4, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the name collision is acceptable. The workaround is to manually name the macro/syntax, or just to not have two copies of the macro (which will cause other problems anyway).

Copy link
Copy Markdown
Member

@gebner gebner Jun 4, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, like in Rust (if I'm not mistaken). It does have the nice effect that stray files (e.g. from a change otherwise stashed away) don't break your build.

Maybe we need to add a script to update Mathlib.lean then. One way or another, CI must complain if somebody adds a file that doesn't build.

Rust will follow transitive dependencies though

The new leanpkg does as well, but this was not a transitive dependency of anything else.. because it's a brand new file.

Copy link
Copy Markdown
Member

@gebner gebner Jun 4, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sadly it seems unavoidable if we want to give parsers reasonable names (so we can open them)

The only surprising thing is that it works just fine if it's in the same file. But this is just something to keep in mind when refactoring.

macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command =>
  `($mods:declModifiers theorem $n $sig $val)
macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command =>
  `($mods:declModifiers theorem $n $sig $val)

@gebner gebner merged commit f8294a6 into leanprover-community:master Jun 9, 2021
@kbuzzard kbuzzard deleted the equiv branch June 9, 2021 16:25
@github-actions github-actions bot mentioned this pull request Dec 19, 2022
Closed
mattrobball added a commit that referenced this pull request Feb 25, 2023
@mattrobball
# This is a combination of 126 commits.
8fcb216 
# This is the 1st commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.IsLimit

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #11 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #12 will be skipped:

# Initial file copy from mathport

# The commit message #13 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #14 will be skipped:

# fix all but one decl

# The commit message #15 will be skipped:

# fix last errors

# The commit message #16 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #17 will be skipped:

# Initial file copy from mathport

# The commit message #18 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #19 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #22 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #25 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #28 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #29 will be skipped:

# Initial file copy from mathport

# The commit message #30 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #31 will be skipped:

# fix some errors

# The commit message #32 will be skipped:

# some more fixes

# The commit message #33 will be skipped:

# more fixes

# The commit message #34 will be skipped:

# finally fixed

# The commit message #35 will be skipped:

# lint

# The commit message #36 will be skipped:

# add porting note for scary warning

# The commit message #37 will be skipped:

# add porting note about proliferation of match

# The commit message #38 will be skipped:

# initial pass

# The commit message #39 will be skipped:

# fix errors

# The commit message #40 will be skipped:

# lint

# The commit message #41 will be skipped:

# fix errors; lint; add porting notes

# The commit message #42 will be skipped:

# fix errors; lint; add porting note

# The commit message #43 will be skipped:

# fix error

# The commit message #44 will be skipped:

# fix some errors

# The commit message #45 will be skipped:

# minor fixes

# The commit message #46 will be skipped:

# fix all but four

# The commit message #47 will be skipped:

# fix last errors; lint

# The commit message #48 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #49 will be skipped:

# Initial file copy from mathport

# The commit message #50 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #51 will be skipped:

# get file to build

# The commit message #52 will be skipped:

# lint

# The commit message #53 will be skipped:

# lint some more

# The commit message #54 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #55 will be skipped:

# Initial file copy from mathport

# The commit message #56 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #57 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #58 will be skipped:

# Initial file copy from mathport

# The commit message #59 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #60 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #61 will be skipped:

# Initial file copy from mathport

# The commit message #62 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #63 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #64 will be skipped:

# Initial file copy from mathport

# The commit message #65 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #66 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #67 will be skipped:

# Initial file copy from mathport

# The commit message #68 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #69 will be skipped:

# first pass

# The commit message #70 will be skipped:

# names and removing restate_axiom

# The commit message #71 will be skipped:

# fix lint

# The commit message #72 will be skipped:

# remove spurious edit

# The commit message #73 will be skipped:

# fix errors; lint

# The commit message #74 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #75 will be skipped:

# Initial file copy from mathport

# The commit message #76 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #77 will be skipped:

# Initial file copy from mathport

# The commit message #78 will be skipped:

# Mathbin -> Mathlib; add import to Mathlib.lean

# The commit message #79 will be skipped:

# push it as far as possible

# The commit message #80 will be skipped:

# minor changes

# The commit message #81 will be skipped:

# seems to work

# The commit message #82 will be skipped:

# add example and equivalence file for testing

# The commit message #83 will be skipped:

# test: create `slice.lean` test file

# The commit message #84 will be skipped:

# remove equivalence.lean

# The commit message #85 will be skipped:

# remove rewriteTarget'; change MonadExceptOf to MonadExcept

# The commit message #86 will be skipped:

# add documentation and clean up

# The commit message #87 will be skipped:

# move iteration tactics to core

# The commit message #88 will be skipped:

# modify documentation lines

# The commit message #89 will be skipped:

# add module documentation(?)

# The commit message #90 will be skipped:

# fix module docs

# The commit message #91 will be skipped:

# fix test/slice.lean

# The commit message #92 will be skipped:

# fix all but refl error

# The commit message #93 will be skipped:

# fix refl error and lint errors

# The commit message #94 will be skipped:

# fix final long line

# The commit message #95 will be skipped:

# use `Mathport` syntax
# * use existing docs
# * fix docs typos

# The commit message #96 will be skipped:

# test: add simple `rhs`/`lhs` tests

# The commit message #97 will be skipped:

# minor changes to `Tactic.Core`
# * use `m` instead of `TacticM` now that we use `MonadExcept`
# * simplify code for `iterateRange`
# * minor docs tweaks

# The commit message #98 will be skipped:

# update slice naming

# The commit message #99 will be skipped:

# some progress

# The commit message #100 will be skipped:

# only one error left

# The commit message #101 will be skipped:

# filled in last sorry

# The commit message #102 will be skipped:

# break long lines

# The commit message #103 will be skipped:

# delete linter command

# The commit message #104 will be skipped:

# fix comments

# The commit message #105 will be skipped:

# fix two simpNF lints

# The commit message #106 will be skipped:

# fill in some docstrings

# The commit message #107 will be skipped:

# fix most linter issues

# The commit message #108 will be skipped:

# add missing aligns for fields; lint

# The commit message #109 will be skipped:

# restore lost import line

# The commit message #110 will be skipped:

# fix errors; lint

# The commit message #111 will be skipped:

# feat: port CategoryTheory.Limits.Shapes.StrongEpi

# The commit message #112 will be skipped:

# Initial file copy from mathport

# The commit message #113 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #114 will be skipped:

# fix errors; lint

# The commit message #115 will be skipped:

# Update Mathlib.lean

# The commit message #116 will be skipped:

# fix errors; lint

# The commit message #117 will be skipped:

# fix errors; lint; shorten filename

# The commit message #118 will be skipped:

# fix some errors

# The commit message #119 will be skipped:

# fix some more

# The commit message #120 will be skipped:

# fix errors

# The commit message #121 will be skipped:

# lint

# The commit message #122 will be skipped:

# fix errors

# The commit message #123 will be skipped:

# lint

# The commit message #124 will be skipped:

# feat: port CategoryTheory.Category.Ulift

# The commit message #125 will be skipped:

# Initial file copy from mathport

# The commit message #126 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean
mattrobball added a commit that referenced this pull request Feb 25, 2023
@mattrobball
# This is a combination of 90 commits.
20f5a8f 
# This is the 1st commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #11 will be skipped:

# fix all but one decl

# The commit message #12 will be skipped:

# fix last errors

# The commit message #13 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #14 will be skipped:

# Initial file copy from mathport

# The commit message #15 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #16 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #17 will be skipped:

# Initial file copy from mathport

# The commit message #18 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #19 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #22 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #25 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #28 will be skipped:

# fix some errors

# The commit message #29 will be skipped:

# some more fixes

# The commit message #30 will be skipped:

# more fixes

# The commit message #31 will be skipped:

# finally fixed

# The commit message #32 will be skipped:

# lint

# The commit message #33 will be skipped:

# add porting note for scary warning

# The commit message #34 will be skipped:

# add porting note about proliferation of match

# The commit message #35 will be skipped:

# initial pass

# The commit message #36 will be skipped:

# fix errors

# The commit message #37 will be skipped:

# lint

# The commit message #38 will be skipped:

# fix errors; lint; add porting notes

# The commit message #39 will be skipped:

# fix errors; lint; add porting note

# The commit message #40 will be skipped:

# fix error

# The commit message #41 will be skipped:

# fix some errors

# The commit message #42 will be skipped:

# minor fixes

# The commit message #43 will be skipped:

# fix all but four

# The commit message #44 will be skipped:

# Delete start_port-macos.sh

# The commit message #45 will be skipped:

# fix last errors; lint

# The commit message #46 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #47 will be skipped:

# Initial file copy from mathport

# The commit message #48 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #49 will be skipped:

# get file to build

# The commit message #50 will be skipped:

# lint

# The commit message #51 will be skipped:

# lint some more

# The commit message #52 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #53 will be skipped:

# Initial file copy from mathport

# The commit message #54 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #55 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #56 will be skipped:

# Initial file copy from mathport

# The commit message #57 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #58 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #59 will be skipped:

# Initial file copy from mathport

# The commit message #60 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #61 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #62 will be skipped:

# Initial file copy from mathport

# The commit message #63 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #64 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #65 will be skipped:

# Initial file copy from mathport

# The commit message #66 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #67 will be skipped:

# first pass

# The commit message #68 will be skipped:

# names and removing restate_axiom

# The commit message #69 will be skipped:

# fix lint

# The commit message #70 will be skipped:

# remove spurious edit

# The commit message #71 will be skipped:

# fix errors; lint

# The commit message #72 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #73 will be skipped:

# Initial file copy from mathport

# The commit message #74 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #75 will be skipped:

# Initial file copy from mathport

# The commit message #76 will be skipped:

# Mathbin -> Mathlib; add import to Mathlib.lean

# The commit message #77 will be skipped:

# push it as far as possible

# The commit message #78 will be skipped:

# minor changes

# The commit message #79 will be skipped:

# seems to work

# The commit message #80 will be skipped:

# add example and equivalence file for testing

# The commit message #81 will be skipped:

# test: create `slice.lean` test file

# The commit message #82 will be skipped:

# remove equivalence.lean

# The commit message #83 will be skipped:

# remove rewriteTarget'; change MonadExceptOf to MonadExcept

# The commit message #84 will be skipped:

# add documentation and clean up

# The commit message #85 will be skipped:

# move iteration tactics to core

# The commit message #86 will be skipped:

# add slice to global import file

# The commit message #87 will be skipped:

# modify documentation lines

# The commit message #88 will be skipped:

# add module documentation(?)

# The commit message #89 will be skipped:

# fix module docs

# The commit message #90 will be skipped:

# fix test/slice.lean
mattrobball added a commit that referenced this pull request Mar 1, 2023
@mattrobball
Squashed commit of the following:
2807219 
commit 6a44854
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 28 06:29:46 2023 -0500

    add missing aligns to cones.lean

commit 84ea4c6
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 14:55:26 2023 -0500

    lint for changes and clean up

commit 3ef0e8b
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 14:12:15 2023 -0500

    golf (co)yoneda proofs

commit 16bd36d
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 12:53:09 2023 -0500

    remove extra instances

commit 21f6296
Merge: 1985f48 5107462
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 06:47:34 2023 -0500

    Merge branch 'master' into port/CategoryTheory.Limits.HasLimits

commit 1985f48
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 06:46:53 2023 -0500

    add updated dependencies

commit d862b81
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 21:42:30 2023 -0500

    fix long line

commit 51660c6
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 21:39:24 2023 -0500

    change X to pt

commit e708679
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 21:30:52 2023 -0500

    revert one more

commit 69b5d00
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 21:30:10 2023 -0500

    fix rebase

commit 5f289c1
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 20:52:34 2023 -0500

    fix import file

commit d3d56ee
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 21 23:16:12 2023 -0500

    move names to new convention

commit 9dfd1d9
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 21 23:02:58 2023 -0500

    add updated files

commit 90d60fc
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 19 19:19:52 2023 -0500

    fix case error

commit 6979193
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 19 00:02:32 2023 -0500

    fix import line typo

commit 843cf69
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:52:06 2023 -0500

    fix import file

commit 4534cda
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:51:22 2023 -0500

    align names in comments

commit 4dfea81
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:38:31 2023 -0500

    lint for CI

commit 6373462
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:28:31 2023 -0500

    try fix-comments.py

    only fixed a single issue for the second time now

commit a45d823
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:26:14 2023 -0500

    fix final error

commit f7dcf96
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:22:54 2023 -0500

    fix all but one decl

commit 2f25984
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 20:50:11 2023 -0500

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

commit f1c2148
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 20:49:48 2023 -0500

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

commit 8fcb216
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 21:19:06 2023 -0500

    # This is a combination of 126 commits.
    # This is the 1st commit message:

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

    # The commit message #2 will be skipped:

    # feat: port CategoryTheory.Limits.IsLimit

    # The commit message #3 will be skipped:

    # Initial file copy from mathport

    # The commit message #4 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #5 will be skipped:

    # feat: port CategoryTheory.Limits.Cones

    # The commit message #6 will be skipped:

    # Initial file copy from mathport

    # The commit message #7 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #8 will be skipped:

    # feat: port CategoryTheory.Yoneda

    # The commit message #9 will be skipped:

    # Initial file copy from mathport

    # The commit message #10 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #11 will be skipped:

    # feat: port CategoryTheory.Functor.Currying

    # The commit message #12 will be skipped:

    # Initial file copy from mathport

    # The commit message #13 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #14 will be skipped:

    # fix all but one decl

    # The commit message #15 will be skipped:

    # fix last errors

    # The commit message #16 will be skipped:

    # feat: port CategoryTheory.Functor.Hom

    # The commit message #17 will be skipped:

    # Initial file copy from mathport

    # The commit message #18 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #19 will be skipped:

    # feat: port CategoryTheory.Types

    # The commit message #20 will be skipped:

    # Initial file copy from mathport

    # The commit message #21 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #22 will be skipped:

    # feat: port CategoryTheory.EpiMono

    # The commit message #23 will be skipped:

    # Initial file copy from mathport

    # The commit message #24 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #25 will be skipped:

    # feat: port CategoryTheory.Groupoid

    # The commit message #26 will be skipped:

    # Initial file copy from mathport

    # The commit message #27 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #28 will be skipped:

    # feat: port CategoryTheory.Pi.Basic

    # The commit message #29 will be skipped:

    # Initial file copy from mathport

    # The commit message #30 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #31 will be skipped:

    # fix some errors

    # The commit message #32 will be skipped:

    # some more fixes

    # The commit message #33 will be skipped:

    # more fixes

    # The commit message #34 will be skipped:

    # finally fixed

    # The commit message #35 will be skipped:

    # lint

    # The commit message #36 will be skipped:

    # add porting note for scary warning

    # The commit message #37 will be skipped:

    # add porting note about proliferation of match

    # The commit message #38 will be skipped:

    # initial pass

    # The commit message #39 will be skipped:

    # fix errors

    # The commit message #40 will be skipped:

    # lint

    # The commit message #41 will be skipped:

    # fix errors; lint; add porting notes

    # The commit message #42 will be skipped:

    # fix errors; lint; add porting note

    # The commit message #43 will be skipped:

    # fix error

    # The commit message #44 will be skipped:

    # fix some errors

    # The commit message #45 will be skipped:

    # minor fixes

    # The commit message #46 will be skipped:

    # fix all but four

    # The commit message #47 will be skipped:

    # fix last errors; lint

    # The commit message #48 will be skipped:

    # feat: port CategoryTheory.DiscreteCategory

    # The commit message #49 will be skipped:

    # Initial file copy from mathport

    # The commit message #50 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #51 will be skipped:

    # get file to build

    # The commit message #52 will be skipped:

    # lint

    # The commit message #53 will be skipped:

    # lint some more

    # The commit message #54 will be skipped:

    # feat: port CategoryTheory.Functor.ReflectsIsomorphisms

    # The commit message #55 will be skipped:

    # Initial file copy from mathport

    # The commit message #56 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #57 will be skipped:

    # feat: port CategoryTheory.Functor.EpiMono

    # The commit message #58 will be skipped:

    # Initial file copy from mathport

    # The commit message #59 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #60 will be skipped:

    # feat: port CategoryTheory.LiftingProperties.Adjunction

    # The commit message #61 will be skipped:

    # Initial file copy from mathport

    # The commit message #62 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #63 will be skipped:

    # feat: port CategoryTheory.LiftingProperties.Basic

    # The commit message #64 will be skipped:

    # Initial file copy from mathport

    # The commit message #65 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #66 will be skipped:

    # feat: port CategoryTheory.CommSq

    # The commit message #67 will be skipped:

    # Initial file copy from mathport

    # The commit message #68 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #69 will be skipped:

    # first pass

    # The commit message #70 will be skipped:

    # names and removing restate_axiom

    # The commit message #71 will be skipped:

    # fix lint

    # The commit message #72 will be skipped:

    # remove spurious edit

    # The commit message #73 will be skipped:

    # fix errors; lint

    # The commit message #74 will be skipped:

    # feat: port CategoryTheory.Adjunction.Basic

    # The commit message #75 will be skipped:

    # Initial file copy from mathport

    # The commit message #76 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #77 will be skipped:

    # Initial file copy from mathport

    # The commit message #78 will be skipped:

    # Mathbin -> Mathlib; add import to Mathlib.lean

    # The commit message #79 will be skipped:

    # push it as far as possible

    # The commit message #80 will be skipped:

    # minor changes

    # The commit message #81 will be skipped:

    # seems to work

    # The commit message #82 will be skipped:

    # add example and equivalence file for testing

    # The commit message #83 will be skipped:

    # test: create `slice.lean` test file

    # The commit message #84 will be skipped:

    # remove equivalence.lean

    # The commit message #85 will be skipped:

    # remove rewriteTarget'; change MonadExceptOf to MonadExcept

    # The commit message #86 will be skipped:

    # add documentation and clean up

    # The commit message #87 will be skipped:

    # move iteration tactics to core

    # The commit message #88 will be skipped:

    # modify documentation lines

    # The commit message #89 will be skipped:

    # add module documentation(?)

    # The commit message #90 will be skipped:

    # fix module docs

    # The commit message #91 will be skipped:

    # fix test/slice.lean

    # The commit message #92 will be skipped:

    # fix all but refl error

    # The commit message #93 will be skipped:

    # fix refl error and lint errors

    # The commit message #94 will be skipped:

    # fix final long line

    # The commit message #95 will be skipped:

    # use `Mathport` syntax
    # * use existing docs
    # * fix docs typos

    # The commit message #96 will be skipped:

    # test: add simple `rhs`/`lhs` tests

    # The commit message #97 will be skipped:

    # minor changes to `Tactic.Core`
    # * use `m` instead of `TacticM` now that we use `MonadExcept`
    # * simplify code for `iterateRange`
    # * minor docs tweaks

    # The commit message #98 will be skipped:

    # update slice naming

    # The commit message #99 will be skipped:

    # some progress

    # The commit message #100 will be skipped:

    # only one error left

    # The commit message #101 will be skipped:

    # filled in last sorry

    # The commit message #102 will be skipped:

    # break long lines

    # The commit message #103 will be skipped:

    # delete linter command

    # The commit message #104 will be skipped:

    # fix comments

    # The commit message #105 will be skipped:

    # fix two simpNF lints

    # The commit message #106 will be skipped:

    # fill in some docstrings

    # The commit message #107 will be skipped:

    # fix most linter issues

    # The commit message #108 will be skipped:

    # add missing aligns for fields; lint

    # The commit message #109 will be skipped:

    # restore lost import line

    # The commit message #110 will be skipped:

    # fix errors; lint

    # The commit message #111 will be skipped:

    # feat: port CategoryTheory.Limits.Shapes.StrongEpi

    # The commit message #112 will be skipped:

    # Initial file copy from mathport

    # The commit message #113 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #114 will be skipped:

    # fix errors; lint

    # The commit message #115 will be skipped:

    # Update Mathlib.lean

    # The commit message #116 will be skipped:

    # fix errors; lint

    # The commit message #117 will be skipped:

    # fix errors; lint; shorten filename

    # The commit message #118 will be skipped:

    # fix some errors

    # The commit message #119 will be skipped:

    # fix some more

    # The commit message #120 will be skipped:

    # fix errors

    # The commit message #121 will be skipped:

    # lint

    # The commit message #122 will be skipped:

    # fix errors

    # The commit message #123 will be skipped:

    # lint

    # The commit message #124 will be skipped:

    # feat: port CategoryTheory.Category.Ulift

    # The commit message #125 will be skipped:

    # Initial file copy from mathport

    # The commit message #126 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

commit e22a9d9
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 21:19:06 2023 -0500

    Initial file copy from mathport

commit f875c67
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 21:19:06 2023 -0500

    feat: port CategoryTheory.Limits.HasLimits
mattrobball added a commit that referenced this pull request Mar 1, 2023
@mattrobball
# This is a combination of 87 commits.
5b01e46 
# This is the 1st commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.HasLimits

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Limits.IsLimit

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #11 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #12 will be skipped:

# Initial file copy from mathport

# The commit message #13 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #14 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #15 will be skipped:

# Initial file copy from mathport

# The commit message #16 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #17 will be skipped:

# fix all but one decl

# The commit message #18 will be skipped:

# fix last errors

# The commit message #19 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #22 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #25 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #28 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #29 will be skipped:

# Initial file copy from mathport

# The commit message #30 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #31 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #32 will be skipped:

# Initial file copy from mathport

# The commit message #33 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #34 will be skipped:

# fix some errors

# The commit message #35 will be skipped:

# some more fixes

# The commit message #36 will be skipped:

# more fixes

# The commit message #37 will be skipped:

# finally fixed

# The commit message #38 will be skipped:

# lint

# The commit message #39 will be skipped:

# add porting note for scary warning

# The commit message #40 will be skipped:

# add porting note about proliferation of match

# The commit message #41 will be skipped:

# initial pass

# The commit message #42 will be skipped:

# fix errors

# The commit message #43 will be skipped:

# lint

# The commit message #44 will be skipped:

# fix errors; lint; add porting notes

# The commit message #45 will be skipped:

# fix errors; lint; add porting note

# The commit message #46 will be skipped:

# fix error

# The commit message #47 will be skipped:

# fix some errors

# The commit message #48 will be skipped:

# minor fixes

# The commit message #49 will be skipped:

# fix all but four

# The commit message #50 will be skipped:

# Delete start_port-macos.sh

# The commit message #51 will be skipped:

# fix last errors; lint

# The commit message #52 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #53 will be skipped:

# Initial file copy from mathport

# The commit message #54 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #55 will be skipped:

# get file to build

# The commit message #56 will be skipped:

# lint

# The commit message #57 will be skipped:

# lint some more

# The commit message #58 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #59 will be skipped:

# Initial file copy from mathport

# The commit message #60 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #61 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #62 will be skipped:

# Initial file copy from mathport

# The commit message #63 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #64 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #65 will be skipped:

# Initial file copy from mathport

# The commit message #66 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #67 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #68 will be skipped:

# Initial file copy from mathport

# The commit message #69 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #70 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #71 will be skipped:

# Initial file copy from mathport

# The commit message #72 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #73 will be skipped:

# first pass

# The commit message #74 will be skipped:

# names and removing restate_axiom

# The commit message #75 will be skipped:

# fix lint

# The commit message #76 will be skipped:

# remove spurious edit

# The commit message #77 will be skipped:

# fix errors; lint

# The commit message #78 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #79 will be skipped:

# Initial file copy from mathport

# The commit message #80 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #81 will be skipped:

# Initial file copy from mathport

# The commit message #82 will be skipped:

# Mathbin -> Mathlib; add import to Mathlib.lean

# The commit message #83 will be skipped:

# push it as far as possible

# The commit message #84 will be skipped:

# minor changes

# The commit message #85 will be skipped:

# seems to work

# The commit message #86 will be skipped:

# add example and equivalence file for testing

# The commit message #87 will be skipped:

# test: create `slice.lean` test file
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 14, 2025
@jessealama
feat: Euler's polyhedron formula via homological algebra
e6f3873 
Proves V - E + F = 2 for convex polyhedra (Wiedijk theorem leanprover-community#13).

Approach: Uses chain complexes and homological algebra to establish
that for an acyclic polyhedron, the Euler characteristic equals 2.

Main contributions:
- GeometricPolyhedron structure with chain complex property (∂² = 0)
- Augmented complex construction and acyclicity characterization
- Euler characteristic computation via telescoping sum
- Special cases for 1D (polygons) and 2D (surfaces) polyhedra

Co-authored-by: Claude <assistant@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 14, 2025
@jessealama
feat: Euler's polyhedron formula via homological algebra
8562369 
Proves V - E + F = 2 for geometric polyhedra (Wiedijk theorem leanprover-community#13).

Approach: Uses chain complexes and homological algebra to establish
that for geometric polyhedra (those satisfying the acyclicity condition),
the Euler characteristic equals 2.

Main contributions:
- GeometricPolyhedron structure with chain complex property (∂² = 0)
- Augmented complex construction and acyclicity characterization
- Euler characteristic computation via telescoping sum
- Special cases for 1D (polygons) and 2D (surfaces) polyhedra

Also adds general lemmas to existing Mathlib modules:
- Telescoping sum theorem in Finset/Basic.lean
- Chain complex Euler characteristic in HomologicalComplex.lean

Co-authored-by: Claude <assistant@anthropic.com>
@jessealama jessealama mentioned this pull request Sep 14, 2025
Closed
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 14, 2025
@jessealama
feat: Euler's polyhedron formula via homological algebra
9c9bd56 
This PR formalizes Euler's polyhedron formula (V - E + F = 2) using homological algebra,
specifically through chain complexes and their Euler characteristics.

Main contributions:
- Define geometric polyhedra with chain complex structure
- Prove that acyclic augmented chain complexes have Euler characteristic 1
- Apply to 2D case to obtain classical V - E + F = 2 formula
- Add to Wiedijk's Formalizing 100 Theorems list (leanprover-community#13)

The proof follows a modern algebraic topology approach, constructing a chain complex
from the polyhedron's face structure and using the vanishing of homology groups to
establish the formula.

Co-authored-by: Jesse Michael Han <jesse@pqr.ai>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 14, 2025
@jessealama
feat: Euler's polyhedron formula via homological algebra
723480b 
This PR formalizes Euler's polyhedron formula (V - E + F = 2) using homological algebra,
specifically through chain complexes and their Euler characteristics.

Main contributions:
- Define geometric polyhedra with chain complex structure
- Prove that acyclic augmented chain complexes have Euler characteristic 1
- Apply to 2D case to obtain classical V - E + F = 2 formula
- Add to Wiedijk's Formalizing 100 Theorems list (leanprover-community#13)

The proof follows a modern algebraic topology approach, constructing a chain complex
from the polyhedron's face structure and using the vanishing of homology groups to
establish the formula.

Co-authored-by: Jesse Michael Han <jesse@pqr.ai>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 14, 2025
@jessealama
feat: Euler's polyhedron formula via homological algebra
b0736e0 
This PR formalizes Euler's polyhedron formula (V - E + F = 2) using homological algebra,
specifically through chain complexes and their Euler characteristics.

Main contributions:
- Define geometric polyhedra with chain complex structure
- Prove that acyclic augmented chain complexes have Euler characteristic 1
- Apply to 2D case to obtain classical V - E + F = 2 formula
- Add to Wiedijk's Formalizing 100 Theorems list (leanprover-community#13)

The proof follows a modern algebraic topology approach, constructing a chain complex
from the polyhedron's face structure and using the vanishing of homology groups to
establish the formula.

Co-authored-by: Jesse Michael Han <jesse@pqr.ai>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 14, 2025
@jessealama
feat: Euler's polyhedron formula via homological algebra
2f7d059 
This PR formalizes Euler's polyhedron formula (V - E + F = 2) using homological algebra,
specifically through chain complexes and their Euler characteristics.

Main contributions:
- Define geometric polyhedra with chain complex structure
- Prove that acyclic augmented chain complexes have Euler characteristic 1
- Apply to 2D case to obtain classical V - E + F = 2 formula
- Add to Wiedijk's Formalizing 100 Theorems list (leanprover-community#13)

The proof follows a modern algebraic topology approach, constructing a chain complex
from the polyhedron's face structure and using the vanishing of homology groups to
establish the formula.

Co-authored-by: Jesse Michael Han <jesse@pqr.ai>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 16, 2025
@jessealama @claude
feat: add Euler-Poincaré formula for chain complexes
c9ece47 
This PR contributes the Euler-Poincaré formula for bounded chain complexes
of finite-dimensional vector spaces over a field.

## Main Contributions

### Core Theorem
* `ChainComplex.euler_poincare_formula`: The Euler-Poincaré formula showing that
  the alternating sum of chain space dimensions equals the alternating sum of
  homology dimensions for bounded complexes

### Supporting Infrastructure
* Euler characteristic definitions in `EulerCharacteristic.lean`:
  - `ChainComplex.boundedEulerChar`: Bounded Euler characteristic
  - `ChainComplex.homologyBoundedEulerChar`: Homological Euler characteristic
* General chain complex lemmas added to `HomologicalComplex.lean`
* Private telescoping sum lemma for the main proof

## Related Work

This is part of a multi-PR contribution towards formalizing Euler's polyhedron
formula (Wiedijk leanprover-community#13). Related to:
- PR leanprover-community#29643 (telescoping sum infrastructure)
- PR leanprover-community#29639 (original combined PR)

## Acknowledgments

Thanks to @joelriou for valuable feedback on the original PR.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 16, 2025
@jessealama @claude
feat: add Euler-Poincaré formula for chain complexes
4d1e774 
Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 16, 2025
@jessealama @claude
feat: add Euler-Poincaré formula for chain complexes
36439f8 
Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 16, 2025
@jessealama @claude
feat: add Euler-Poincaré formula for chain complexes
9d9e37b 
Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 16, 2025
@jessealama @claude
feat: add Euler-Poincaré formula for chain complexes
b48d5c1 
Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 16, 2025
@jessealama @claude
feat: add Euler-Poincaré formula for chain complexes
d402fb9 
Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 16, 2025
@jessealama @claude
feat: add Euler-Poincaré formula for chain complexes
e42702d 
Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 17, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula for bounded chain …
0013812 
…complexes

Proves that the alternating sum of dimensions equals the alternating sum of homology dimensions for bounded chain complexes of finite-dimensional vector spaces.

Main results:
- `ChainComplex.eulerChar_eq_homology_eulerChar`: For ℤ-indexed bounded complexes
- Supporting lemmas for dimension decomposition and telescoping sums
- Definitions for Euler characteristic in `EulerCharacteristic.lean`

This is part of the effort to formalize Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 17, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula for bounded chain …
31d20b0 
…complexes

Proves that the alternating sum of dimensions equals the alternating sum of homology dimensions for bounded chain complexes of finite-dimensional vector spaces.

Main results:
- `ChainComplex.eulerChar_eq_homology_eulerChar`: For ℤ-indexed bounded complexes
- Supporting lemmas for dimension decomposition and telescoping sums
- Definitions for Euler characteristic in `EulerCharacteristic.lean`

This is part of the effort to formalize Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 17, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula for bounded chain …
5af9364 
…complexes

Proves that the alternating sum of dimensions equals the alternating sum of homology dimensions for bounded chain complexes of finite-dimensional vector spaces.

Main results:
- `ChainComplex.eulerChar_eq_homology_eulerChar`: For ℤ-indexed bounded complexes
- Supporting lemmas for dimension decomposition and telescoping sums
- Definitions for Euler characteristic in `EulerCharacteristic.lean`

This is part of the effort to formalize Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
@jessealama jessealama mentioned this pull request Sep 17, 2025
Draft
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 17, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula for bounded chain …
1d6ae71 
…complexes

Proves that the alternating sum of dimensions equals the alternating sum of homology dimensions for bounded chain complexes of finite-dimensional vector spaces.

Main results:
- `ChainComplex.eulerChar_eq_homology_eulerChar`: For ℤ-indexed bounded complexes
- Supporting lemmas for dimension decomposition and telescoping sums
- Definitions for Euler characteristic in `EulerCharacteristic.lean` (ℤ-indexed only)

This is part of the effort to formalize Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 19, 2025
@jessealama
feat(Algebra/Homology): add Euler-Poincaré formula
c1dafb6 
This PR adds the Euler characteristic for chain complexes and proves the Euler-Poincaré formula relating the alternating sum of chain dimensions to the alternating sum of homology dimensions.

Main definitions (in `EulerCharacteristic.lean`):
* `ChainComplex.eulerChar`: The Euler characteristic (alternating sum of dimensions) for a bounded chain complex
* `ChainComplex.homologyEulerChar`: The homological Euler characteristic (alternating sum of homology dimensions)

Both definitions work with ℤ-indexed complexes over any ring R.

Main result (in `EulerPoincare.lean`):
* `ChainComplex.eulerChar_eq_homology_eulerChar`: For ℤ-indexed bounded chain complexes of finite-dimensional modules over a division ring, the alternating sum of chain dimensions equals the alternating sum of homology dimensions.

Supporting infrastructure:
The proof uses:
* Telescoping sum lemmas for alternating sums
* The rank-nullity theorem for linear maps over division rings
* Properties of exact sequences in homology

This is part of a series of PRs building toward a formalization of Euler's polyhedron formula (Wiedijk leanprover-community#13).
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 19, 2025
@jessealama
feat(Algebra/Homology): add Euler-Poincaré formula
ea5d6a3 
This PR adds the Euler characteristic for chain complexes and proves the
Euler-Poincaré formula relating the alternating sum of chain dimensions to
the alternating sum of homology dimensions.

Main definitions (in EulerCharacteristic.lean):
* ChainComplex.eulerChar: The Euler characteristic (alternating sum of dimensions)
* ChainComplex.homologyEulerChar: The homological Euler characteristic
* ChainComplex.boundedEulerChar: Bounded version for finite index sets
* ChainComplex.homologyBoundedEulerChar: Bounded homological version

Main result (in EulerPoincare.lean):
* ChainComplex.eulerChar_eq_homology_eulerChar: For ℤ-indexed bounded chain
  complexes of finite-dimensional modules over a division ring, the alternating
  sum of chain dimensions equals the alternating sum of homology dimensions.

The proof uses telescoping sum lemmas for alternating sums, the rank-nullity
theorem for linear maps over division rings, and properties of exact sequences
in homology.

This is part of a series of PRs building toward a formalization of Euler's
polyhedron formula (Wiedijk leanprover-community#13).
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 21, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler's polyhedron formula
13ed14a 
Adds a formalization of Euler's polyhedron formula (Wiedijk leanprover-community#13) using
homological algebra. The proof establishes V - E + F = 2 for connected
polyhedra by computing the Euler characteristic of the associated chain
complex.

**Main theorem (`EulerPolyhedronFormula.lean`):**
- `euler_polyhedron_formula`: For a connected geometric polyhedron with
  spherical homology, the Euler characteristic equals `1 + (-1)^dim`

**Core machinery (`EulerPolyhedronFormula/Basic.lean`):**
- `GeometricPolyhedron`: Polyhedra with concrete geometric structure
- `toChainComplex`: Construction of chain complex from polyhedron
- `hasSphericalHomology`: Homology concentrated at extremes
- Supporting lemmas for computing dimensions and exactness

This completes the formalization of one of Wiedijk's 100 theorems.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 21, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler's polyhedron formula
f4b8a40 
Adds a formalization of Euler's polyhedron formula (Wiedijk leanprover-community#13) using
homological algebra. The proof establishes V - E + F = 2 for connected
polyhedra by computing the Euler characteristic of the associated chain
complex.

**Main theorem (`EulerPolyhedronFormula.lean`):**
- `euler_polyhedron_formula`: For a connected geometric polyhedron with
  spherical homology, the Euler characteristic equals `1 + (-1)^dim`

**Core machinery (`EulerPolyhedronFormula/Basic.lean`):**
- `GeometricPolyhedron`: Polyhedra with concrete geometric structure
- `toChainComplex`: Construction of chain complex from polyhedron
- `hasSphericalHomology`: Homology concentrated at extremes
- Supporting lemmas for computing dimensions and exactness

This completes the formalization of one of Wiedijk's 100 theorems.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 21, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler's polyhedron formula
cc1492c 
Adds a formalization of Euler's polyhedron formula (Wiedijk leanprover-community#13) using
homological algebra. The proof establishes V - E + F = 2 for connected
polyhedra by computing the Euler characteristic of the associated chain
complex.

**Main theorem (`EulerPolyhedronFormula.lean`):**
- `euler_polyhedron_formula`: For a connected geometric polyhedron with
  spherical homology, the Euler characteristic equals `1 + (-1)^dim`

**Core machinery (`EulerPolyhedronFormula/Basic.lean`):**
- `GeometricPolyhedron`: Polyhedra with concrete geometric structure
- `toChainComplex`: Construction of chain complex from polyhedron
- `hasSphericalHomology`: Homology concentrated at extremes
- Supporting lemmas for computing dimensions and exactness

This completes the formalization of one of Wiedijk's 100 theorems.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 21, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler's polyhedron formula
3c0f316 
Adds a formalization of Euler's polyhedron formula (Wiedijk leanprover-community#13) using
homological algebra. The proof establishes V - E + F = 2 for connected
polyhedra by computing the Euler characteristic of the associated chain
complex.

**Main theorem (`EulerPolyhedronFormula.lean`):**
- `euler_polyhedron_formula`: For a connected geometric polyhedron with
  spherical homology, the Euler characteristic equals `1 + (-1)^dim`

**Core machinery (`EulerPolyhedronFormula/Basic.lean`):**
- `GeometricPolyhedron`: Polyhedra with concrete geometric structure
- `toChainComplex`: Construction of chain complex from polyhedron
- `hasSphericalHomology`: Homology concentrated at extremes
- Supporting lemmas for computing dimensions and exactness

This completes the formalization of one of Wiedijk's 100 theorems.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 21, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler's polyhedron formula
8034092 
Adds a formalization of Euler's polyhedron formula (Wiedijk leanprover-community#13) using
homological algebra. The proof establishes V - E + F = 2 for connected
polyhedra by computing the Euler characteristic of the associated chain
complex.

**Main theorem (`EulerPolyhedronFormula.lean`):**
- `euler_polyhedron_formula`: For a connected geometric polyhedron with
  spherical homology, the Euler characteristic equals `1 + (-1)^dim`

**Core machinery (`EulerPolyhedronFormula/Basic.lean`):**
- `GeometricPolyhedron`: Polyhedra with concrete geometric structure
- `toChainComplex`: Construction of chain complex from polyhedron
- `hasSphericalHomology`: Homology concentrated at extremes
- Supporting lemmas for computing dimensions and exactness

This completes the formalization of one of Wiedijk's 100 theorems.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Sep 21, 2025
@jessealama @claude
feat: add Euler's polyhedron formula (Wiedijk leanprover-community#13)
3698241 
Add a homological proof of Euler's polyhedron formula V - E + F = 2.

This contribution includes:
- Core polyhedron structure and chain complex machinery in EulerPolyhedronFormula/Basic.lean
- Main theorem proving χ(P) = 1 + (-1)^d for spherical polyhedra in EulerPolyhedronFormula.lean
- Classical 2D case V - E + F = 2 as a corollary
- Addition to Wiedijk 100 theorems archive
- Supporting infrastructure for Euler characteristic of chain complexes

The proof uses homological algebra: polyhedra with spherical homology
(H_0 = H_dim = 1, all others 0) have Euler characteristic 1 + (-1)^dim.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Oct 9, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula
edf571e 
This PR adds the Euler-Poincaré formula for chain complexes over fields,
establishing that for a finite chain complex with finite-dimensional
homology groups, the Euler characteristic equals the alternating sum
of homology dimensions.

Main contributions:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula

This is part of the work toward formalizing Euler's polyhedron formula
(Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Oct 21, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula
08c6ec6 
This PR adds the Euler-Poincaré formula for chain complexes over fields,
establishing that for a finite chain complex with finite-dimensional
homology groups, the Euler characteristic equals the alternating sum
of homology dimensions.

Main contributions:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula

This is part of the work toward formalizing Euler's polyhedron formula
(Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Nov 5, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula
413feba 
This PR adds the Euler-Poincaré formula for chain complexes over fields,
establishing that for a finite chain complex with finite-dimensional
homology groups, the Euler characteristic equals the alternating sum
of homology dimensions.

Main contributions:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula

This is part of the work toward formalizing Euler's polyhedron formula
(Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Nov 5, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula
4c50b57 
This PR adds the Euler-Poincaré formula for chain complexes over fields,
establishing that for a finite chain complex with finite-dimensional
homology groups, the Euler characteristic equals the alternating sum
of homology dimensions.

Main contributions:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula

This is part of the work toward formalizing Euler's polyhedron formula
(Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Nov 7, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula
da808a4 
This PR adds the Euler-Poincaré formula for chain complexes over fields,
establishing that for a finite chain complex with finite-dimensional
homology groups, the Euler characteristic equals the alternating sum
of homology dimensions.

Main contributions:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula

This is part of the work toward formalizing Euler's polyhedron formula
(Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Nov 22, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula
722e7be 
This PR adds the Euler-Poincaré formula for chain complexes over fields,
establishing that for a finite chain complex with finite-dimensional
homology groups, the Euler characteristic equals the alternating sum
of homology dimensions.

Main contributions:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula

This is part of the work toward formalizing Euler's polyhedron formula
(Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Nov 30, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula
de13d7b 
This PR adds the Euler-Poincaré formula for chain complexes over fields,
establishing that for a finite chain complex with finite-dimensional
homology groups, the Euler characteristic equals the alternating sum
of homology dimensions.

Main contributions:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula

This is part of the work toward formalizing Euler's polyhedron formula
(Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
jessealama added a commit to jessealama/mathlib4 that referenced this pull request Dec 2, 2025
@jessealama @claude
feat(Algebra/Homology): add Euler-Poincaré formula
57d82e7 
This PR adds the Euler-Poincaré formula for chain complexes over fields,
establishing that for a finite chain complex with finite-dimensional
homology groups, the Euler characteristic equals the alternating sum
of homology dimensions.

Main contributions:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula

This is part of the work toward formalizing Euler's polyhedron formula
(Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@gebner gebner gebner left review comments

@digama0 digama0 digama0 left review comments

+1 more reviewer

@Kha Kha Kha left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@kbuzzard @Kha @gebner @digama0