leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/relation_sentences' into graph_language

awainverse committed 3 years ago

27f22db8

awainverse committed 3 years ago

32501bf8

awainverse committed 3 years ago

dcbe14d7

awainverse committed 3 years ago

71e90c15

awainverse committed 3 years ago

6121e6bb

awainverse committed 3 years ago

af2262f6

awainverse committed 3 years ago

c9617274

split(order/chain): Split off `order.zorn` (#13060)

YaelDillies committed 3 years ago

de503895

feat(model_theory/*): Constructors for low-arity languages and structures (#12960)

awainverse committed 3 years ago

13e08bf3

feat(model_theory/bundled, satisfiability): Bundled models (#12945)

awainverse committed 3 years ago

f1ae6206

feat(combinatorics/simple_graph/connectivity): walk constructor patterns with explicit vertices (#13078)

kmill committed 3 years ago

2861d4eb

feat(topology/algebra/matrix): more continuity lemmas for matrices (#13009)

eric-wieser committed 3 years ago

25ef4f0f

feat(ring_theory/polynomial/pochhammer): generalize a proof from `comm_semiring` to `semiring` (#13024)

adomani committed 3 years ago

0f6eec63

feat(analysis/locally_convex): the topology of weak duals is locally convex (#12623)

mcdoll committed 3 years ago

1b42223a

feat(analysis/locally_convex): closed balanced sets are a basis of the topology (#12786)

mcdoll committed 3 years ago

6405a6ad

lint(algebra/*): fix some lint errors (#13058)

urkud committed 3 years ago

7833dbe4

feat(order/sup_indep): lemmas about `pairwise` and `set.pairwise` (#12590)

eric-wieser committed 3 years ago

ba9ead03

chore(algebra/order/monoid_lemmas): remove exactly same lemmas (#13068)

astrainfinita committed 3 years ago

81c5d17e

feat(ring_theory/polynomial/pochhammer): add a binomial like recursion for pochhammer (#13018)

adomani committed 3 years ago

7a37490c

feat(order/category/Semilattice): The categories of semilattices (#12890)

YaelDillies committed 3 years ago

290f440a

refactor(*): rename `topological_ring` to `topological_semiring` and introduce a new `topological_ring` extending `has_continuous_neg` (#12864)

j-loreaux committed 3 years ago

760f1b2b

feat(algebraic_topology): map_alternating_face_map_complex (#13028)

joelriou committed 3 years ago

c2339caa

feat(combinatorics/simple_graph/regularity/bound): Numerical bounds for Szemerédi's regularity lemma (#12962)

YaelDillies committed 3 years ago

8a213165

feat(combinatorics/simple_graph/uniform): Graph uniformity and uniform partitions (#12957)

YaelDillies committed 3 years ago

299984b4

feat(linear_algebra/matrix): any matrix power can be expressed as sums of powers `0 ≤ k < fintype.card n` (#12983)

eric-wieser committed 3 years ago

47b1d786

chore(data/finset/card): add `card_disj_union` (#13061)

eric-wieser committed 3 years ago

fc35cb32

feat(topology/sets/order): Clopen upper sets (#12670)

YaelDillies committed 3 years ago

7f450cb8

feat(topology): add lemmas about `frontier` (#13054)

urkud committed 3 years ago

518e81a8

chore(data/set/pointwise): Golf using `set.image2` API (#13051)

YaelDillies committed 3 years ago

de62b061

feat(analysis/special_functions/pow): abs value of real to complex power (#13048)

loefflerd committed 3 years ago

25e8730e

Older