leanprover-community/mathlib

Pull Requests Commits

feat(order/well_founded): Well founded relations are asymmetric and irreflexive (#13692)

vihdzp committed 4 years ago

e1f00bc7

feat(algebra/module/torsion): torsion ideal, decomposition lemma (#13414)

pbazin committed 4 years ago

6c7b880e

move(set_theory/ordinal/{arithmetic → fixed_points}): Move `nfp` (#13315)

vihdzp committed 4 years ago

e24f7f7a

feat(measure_theory/function/l1_space): add `integrable_smul_measure` (#13922)

urkud committed 4 years ago

1a862493

chore(ring_theory/polynomial/basic): golf polynomial_not_is_field (#13919)

Ruben-VandeVelde committed 4 years ago

af4c6c8a

feat(data/finset/prod): diag of union (#13916)

b-mehta committed 4 years ago

d0efe252

feat(category_theory/simple): nonzero morphisms to/from a simple are epi/mono (#13905)

kim-em committed 4 years ago

098ab17f

refactor(group_theory/{submonoid, subsemigroup}/{center, centralizer}): move set.center and set.centralizer into subsemigroup (#13903)

j-loreaux committed 4 years ago

455393d3

feat(ring_theory/valuation/valuation_subring): Adds some equivalent conditions for equivalence of valuations (#13895)

adamtopaz committed 4 years ago

e6b84992

feat(data/list/basic): add `list.cons_diff` (#13892)

urkud committed 4 years ago

6d370064

feat(analysis/matrix): add `frobenius_norm_conj_transpose` (#13883)

eric-wieser committed 4 years ago

269bc85d

feat(category_theory/simple): simple objects are indecomposable (#13882)

kim-em committed 4 years ago

d537897a

feat(linear_algebra/trace): more general versions of `trace_mul_comm` and `trace_conj` (#13874)

antoinelab01 committed 4 years ago

1afdaf96

feat(topology/algebra/star): continuity of `star` (#13855)

eric-wieser committed 4 years ago

517aa8b6

feat(analysis/asymptotics/specific_asymptotics): Cesaro averaging preserves convergence (#13825)

sgouezel committed 4 years ago

35c8980d

feat(algebra/squarefree): relate squarefree on naturals to factorization (#13816)

b-mehta committed 4 years ago

6e003306

feat(set_theory/game/pgame): Add more congr lemmas (#13808)

vihdzp committed 4 years ago

ba4bf545

feat(algebra/category/FinVect): has finite limits (#13793)

kim-em committed 4 years ago

85657f1b

feat(algebra/hom/non_unital_alg): some constructions for `prod` (#13785)

eric-wieser committed 4 years ago

e3d38edb

refactor(set_theory/game/pgame): Redefine `subsequent` (#13752)

vihdzp committed 4 years ago

9015d2ad

feat(model_theory/satisfiability): A union of a directed family of satisfiable theories is satisfiable (#13750)

awainverse committed 4 years ago

b337b921

feat(model_theory/elementary_maps): The elementary diagram of a structure (#13724)

awainverse committed 4 years ago

51d81675

refactor(linear_algebra/*): more generalisations (#13668)

kim-em committed 4 years ago

319d5028

feat(set_theory/game/pgame): Tweak `pgame.mul` API (#13651)

vihdzp committed 4 years ago

36c5faac

feat(topology/bornology): add more instances (#13621)

urkud committed 4 years ago

bd23639b

feat(set_theory/game/pgame): Tweak `pgame.neg` API (#13617)

vihdzp committed 4 years ago

2402b4d8

chore(analysis): use nnnorm notation everywhere (#13930)

eric-wieser committed 4 years ago

58de2a0a

chore(number_theory/legendre_symbol/quadratic_char): golf some proofs (#13926)

Ruben-VandeVelde committed 4 years ago

6f3426cf

chore(algebra/order/floor): missing simp lemmas on floor of nat and int (#13904)

eric-wieser committed 4 years ago

171825a9

feat(category_theory/bicategory/coherence_tactic): coherence tactic for bicategories (#13417)

yuma-mizuno committed 4 years ago

4d0b6301

Newer Older