mathlib3
feat(combinatorics.simple_graph.ends): A version of Freudenthal-Hopf
#18681
Open
Overview
Commits
149
Changes
View On GitHub
Commits
  • merge
    bottine committed 3 years ago
  • cleanup?
    bottine committed 3 years ago
  • inf_comp_out
    bottine committed 3 years ago
  • Update src/combinatorics/simple_graph/ends/defs.lean
    bottine committed 3 years ago
  • cosmetic
    bottine committed 3 years ago
  • docstrings
    bottine committed 3 years ago
  • Expand subtype in `out_hom` and golf proofs
    0art0 committed 3 years ago
  • Merge branch 'bottine/simple_graph/ends_for_real_this_time' of https://github.com/leanprover-community/mathlib into bottine/simple_graph/ends_for_real_this_time
    0art0 committed 3 years ago
  • Erase `diff` artefact
    0art0 committed 3 years ago
  • finite graphs have no end
    bottine committed 3 years ago
  • docstring
    bottine committed 3 years ago
  • Apply suggestions from code review
    bottine committed 3 years ago
  • errors
    bottine committed 3 years ago
  • errors'
    bottine committed 3 years ago
  • op
    bottine committed 3 years ago
  • Update src/combinatorics/simple_graph/ends/properties.lean
    bottine committed 3 years ago
  • comp_out.hom reverse order and error
    bottine committed 3 years ago
  • better names
    bottine committed 3 years ago
  • Yael's suggestion
    bottine committed 3 years ago
  • forgot this
    bottine committed 3 years ago
  • Apply suggestions from code review
    bottine committed 3 years ago
  • Kyle's suggestions
    bottine committed 3 years ago
  • Update src/combinatorics/simple_graph/ends/defs.lean
    0art0 committed 3 years ago
  • Kyle's suggestions
    bottine committed 3 years ago
  • a few lemmas + tweaks
    bottine committed 3 years ago
  • some golf
    bottine committed 3 years ago
  • some of Yael's suggestions
    bottine committed 3 years ago
  • better
    bottine committed 3 years ago
  • tweaks
    bottine committed 3 years ago
  • Yael's suggestions
    bottine committed 3 years ago
  • details
    bottine committed 3 years ago
  • Yael's suggestions
    bottine committed 3 years ago
  • Update src/combinatorics/simple_graph/ends/defs.lean
    bottine committed 3 years ago
  • Update src/combinatorics/simple_graph/ends/defs.lean
    bottine committed 3 years ago
  • minor
    bottine committed 3 years ago
  • Merge branch 'bottine/simple_graph/ends_for_real_this_time' of ssh://github.com/leanprover-community/mathlib into bottine/simple_graph/ends_for_real_this_time
    bottine committed 3 years ago
  • Junyan's suggestions
    bottine committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into bottine/simple_graph/ends_for_real_this_time
    bottine committed 3 years ago
  • Junyan's suggestions
    bottine committed 3 years ago
  • s/comp_out/component_compl/g
    bottine committed 3 years ago
  • some of Junyan's suggestions
    bottine committed 3 years ago
  • Update src/combinatorics/simple_graph/ends/defs.lean
    bottine committed 3 years ago
  • init.
    bottine committed 3 years ago
  • move lemma
    bottine committed 3 years ago
  • fix
    bottine committed 3 years ago
  • comment
    bottine committed 3 years ago
  • moved lemma
    bottine committed 3 years ago
  • merge
    bottine committed 3 years ago
  • merge+
    bottine committed 3 years ago
  • minigolf
    bottine committed 3 years ago
  • dirty commit
    bottine committed 3 years ago
  • dirty commit
    bottine committed 3 years ago
  • very dirty commit
    bottine committed 3 years ago
  • sorrys
    bottine committed 3 years ago
  • Yael's suggestions
    bottine committed 3 years ago
  • Update defs.lean
    bottine committed 3 years ago
  • Update src/combinatorics/simple_graph/ends/defs.lean
    bottine committed 3 years ago
  • dunno
    bottine committed 3 years ago
  • Prove `induce_induce`
    0art0 committed 3 years ago
  • `induce_induce` code clean-up
    0art0 committed 3 years ago
  • messy
    bottine committed 3 years ago
  • a lemma
    bottine committed 3 years ago
  • Merge branch 'bottine/simple_graph.ends/Freudenthal_Hopf' of ssh://github.com/leanprover-community/mathlib into bottine/simple_graph.ends/Freudenthal_Hopf
    bottine committed 3 years ago
  • minigolf
    bottine committed 3 years ago
  • move lemma
    bottine committed 3 years ago
  • use lemma
    bottine committed 3 years ago
  • wip
    bottine committed 3 years ago
  • wip
    bottine committed 3 years ago
  • yael's suggestion
    bottine committed 3 years ago
  • minigolf
    bottine committed 3 years ago
  • lemmaization
    bottine committed 3 years ago
  • cleaner sorrys
    bottine committed 3 years ago
  • more better sorrys
    bottine committed 3 years ago
  • minigolf
    bottine committed 3 years ago
  • mimniganiset
    bottine committed 3 years ago
  • minigolf''
    bottine committed 3 years ago
  • suite
    bottine committed 3 years ago
  • wip
    bottine committed 3 years ago
  • wip
    bottine committed 3 years ago
  • wip
    bottine committed 3 years ago
  • suite
    bottine committed 3 years ago
  • dirty
    bottine committed 3 years ago
  • wip mittag_leffler
    bottine committed 3 years ago
  • wip m-l
    bottine committed 3 years ago
  • m-l cleanup
    bottine committed 3 years ago
  • m-l cleanup
    bottine committed 3 years ago
  • sorry--
    bottine committed 3 years ago
  • minor
    bottine committed 3 years ago
  • minor
    bottine committed 3 years ago
  • skeletal lemma
    bottine committed 3 years ago
  • lowol
    bottine committed 3 years ago
  • lowowowl
    bottine committed 3 years ago
  • wip
    bottine committed 3 years ago
  • wip file added
    bottine committed 3 years ago
  • starting with the 'extension' lemma
    bottine committed 3 years ago
  • Reorganise according to new plan
    0art0 committed 3 years ago
  • Proofs of various properties
    0art0 committed 3 years ago
  • wip
    bottine committed 3 years ago
  • Prove `induce.iso`
    0art0 committed 3 years ago
  • Proof of `iso_equiv_supp`
    0art0 committed 3 years ago
  • + more commits ...
FAQ Terms Privacy Refunds Impressum
Loading