leanprover-community/mathlib

Pull Requests Commits

Homomorphisms of graphs

kmill committed 5 years ago

e3fd9d3f

Cleaned out older attempts

kmill committed 5 years ago

410293f5

documented sym2 and moved it to data/sym2.lean

kmill committed 5 years ago

5ffe8033

removed comment from sym2

kmill committed 5 years ago

ede3c3ce

experiment basic4 seems to be the best metonymic approach so far

kmill committed 5 years ago

867bc5ea

going with chou formalization. added theorems about sym2 (thanks to david wärn)

kmill committed 5 years ago

874ea215

added some fintype instances

kmill committed 5 years ago

de10f35d

put vertex and edge types outside structure. this seems like a good idea. getting the opposite of an edge from a vertex is still noncomputable, though

kmill committed 5 years ago

f82572d6

experimented with putting the vertex type inside the structure

kmill committed 5 years ago

b65e5132

tried a graph definition that is a fusion of hedetniemi and chou, but can't define function that gives vertex opposite an edge

kmill committed 5 years ago

e824f925

first experiments with this definition of graphs

kmill committed 5 years ago

ff44a03c

feat(data/nat/digits): add digits_lt_base (#3246)

kbuzzard committed 5 years ago

1a419a9f

chore(*): work on removing deprecated is_X_hom typeclasses (#3258)

kim-em committed 5 years ago

f00b7c0c

feat(field_theory/separable): relating irreducibility and separability (#3198)

kckennylau committed 5 years ago

e803c851

chore(data/set/basic): simp attribute on mem_range_self (#3260)

sgouezel committed 5 years ago

a7cdab5d

chore(data/finset, data/multiset): split into smaller files (#3256)

kim-em committed 5 years ago

7bd19b32

feat(category/preadditive): properties of preadditive biproducts (#3245)

kim-em committed 5 years ago

8ba7595a

chore(algebra/big_operators): don't use omega (#3255)

kim-em committed 5 years ago

aff951a5

feat(ring_theory/valuation): definition and basic properties of valuations (#3222)

jcommelin committed 5 years ago

e68503ad

chore(algebra/group_with_zero): nolint (#3254)

bryangingechen committed 5 years ago

a22cd4d7

chore(scripts): update nolints.txt (#3253)

leanprover-community-bot committed 5 years ago

859edfb0

feat(data/matrix): std_basis_matrix (#3244)

kim-em committed 5 years ago

89f3bbc2

feat(category_theory/limits/shapes): simp lemmas to decompose pullback_cone.mk.fst (#3249)

b-mehta committed 5 years ago

a40be987

chore(topology/*): use dot syntax for some lemmas (#3251)

urkud committed 5 years ago

06256910

feat(algebra/lie_algebra): conjugation transformation for Lie algebras of skew-adjoint endomorphims, matrices (#3229)

Oliver Nash committed 5 years ago

b3915636

chore(ring_theory/polynomial): move `ring_theory.polynomial` to `ring_theory.polynomial.basic` (#3248)

Vierkantor committed 5 years ago

ea961f76

feat(topology): real.image_Icc (#3224)

PatrickMassot committed 5 years ago

9524dee3

fix(tactic/interactive_expr): show let-values in tactic state widget (#3228)

gebner committed 5 years ago

1bc6ebaa

fix(tactic/apply_fun): beta reduction was too aggressive (#3214)

kim-em committed 5 years ago

b82ed0c5

chore(topology/algebra/ordered): use `continuous_at`, rename (#3231)

urkud committed 5 years ago

6d0f40a6

Older