leanprover-community/mathlib

Pull Requests Commits

YaelDillies committed 3 years ago

6d9c9f21

chore(model_theory/elementary_maps): Fix Tarski-Vaught Test (#13102)

awainverse committed 3 years ago

c61f7e88

chore(algebra/order/*): generalisation linter (#13098)

kim-em committed 3 years ago

e6a0a266

chore(order/*): generalisation linter (#13097)

kim-em committed 3 years ago

8a51798c

chore(algebra/group_power/basic): generalisation linter (#13095)

kim-em committed 3 years ago

0e95cadc

chore(algebra/ring/basic): generalisation linter (#13094)

kim-em committed 3 years ago

6652766b

feat(model_theory/basic,language_map): More about `language.mk₂` (#13090)

awainverse committed 3 years ago

e326fe60

chore(group_theory/group_action/*): generalisation linter (#13100)

kim-em committed 3 years ago

873f2685

chore(algebra/*): generalisation linter (#13099)

kim-em committed 3 years ago

3a0c0345

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

leanprover-community-bot committed 3 years ago

9728396e

feat(model_theory/elementary_maps): The Tarski-Vaught test (#12919)

awainverse committed 3 years ago

2b92d080

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

Older