leanprover-community/mathlib3

Pull Requests Commits

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

awainverse committed 3 years ago

51d81675

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

kim-em committed 3 years ago

319d5028

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

vihdzp committed 3 years ago

36c5faac

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

urkud committed 3 years ago

bd23639b

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

vihdzp committed 3 years ago

2402b4d8

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

eric-wieser committed 3 years ago

58de2a0a

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

Ruben-VandeVelde committed 3 years ago

6f3426cf

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

eric-wieser committed 3 years ago

171825a9

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

yuma-mizuno committed 3 years ago

4d0b6301

feat(data/zmod/quotient): The quotient `<a>/stab(b)` is cyclic of order `minimal_period ((+ᵥ) a) b` (#13722)

tb65536 committed 3 years ago

c1f329df

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

leanprover-community-bot committed 3 years ago

a2a873fc

Merge branch 'encode_binary_lemmas' of https://github.com/leanprover-community/mathlib into encode_binary_lemmas

prakol16 committed 3 years ago

125ec508

Fix copyright, minor

prakol16 committed 3 years ago

f50dbd31

feat(set_theory/game/short): Birthday of short games (#13875)

vihdzp committed 3 years ago

dd584384

feat(ring_theory/ideal/local_ring): generalize lemmas to semirings (#13471)

yuma-mizuno committed 3 years ago

fc3de197

fix(.docker/*): update elan URL (#13928)

bryangingechen committed 3 years ago

6c0580a2

feat(topology/metric_space/basic): golf, avoid unfold (#13923)

urkud committed 3 years ago

fd651597

feat(measure_theory/integral/torus_integral): torus integral and its properties (#12892)

CumaKoekmen committed 3 years ago

de07131e

doc(order/countable_dense_linear_order): Fix minor mistake (#13921)

vihdzp committed 3 years ago

9c0dfcd8

refactor(ring_theory/jacobson_ideal): generalize lemmas to non-commutative rings (#13865)

eric-wieser committed 3 years ago

5cfb8dbc

chore(topology/continuous_function/bounded): generalize from `normed_*` to `semi_normed_*` (#13915)

eric-wieser committed 3 years ago

16157f26

feat(number_theory/legendre_symbol/): add some lemmas (#13831)

MichaelStollBayreuth committed 3 years ago

bd1d9359

chore(normed_space/weak_dual): generalize `normed_group` to `semi_normed_group` (#13914)

eric-wieser committed 3 years ago

7d287537

feat(set_theory/game/basic): Inline instances (#13813)

vihdzp committed 3 years ago

86887539

feat(algebra/big_operators/basic): `prod_list_count` and `prod_list_count_of_subset` (#13370)

stuart-presnell committed 3 years ago

5c433d03

doc(analysis/matrix): fix broken LaTeX (#13910)

eric-wieser committed 3 years ago

40b59523

feat(linear_algebra/matrix/trace): add `trace_conj_transpose` (#13888)

eric-wieser committed 3 years ago

1c4d2b7c

feat(order/omega_complete_partial_order): make `continuous_hom.prod.apply` continuous (#13833)

nomeata committed 3 years ago

0f8d7a99

feat(topology/algebra/module/basic): A continuous linear functional is open (#13829)

YaelDillies committed 3 years ago

475a5334

move(data/pi/*): Group `pi` files (#13826)

YaelDillies committed 3 years ago

4cea0a8f

Newer Older