leanprover-community/mathlib

Pull Requests Commits

Merge branch 'reduce_logic_small' into sup

kim-em committed 3 years ago

c18aac1f

kim-em committed 3 years ago

a21cfef0

Merge branch 'split_order_group' into split_order_ring

kim-em committed 3 years ago

682ad40a

kim-em committed 3 years ago

5cf6ce35

kim-em committed 3 years ago

6d283efe

fix downstream import

kim-em committed 3 years ago

a16e98cf

Merge remote-tracking branch 'origin/master' into split_data_int_basic

kim-em committed 3 years ago

8423f3fc

fix(geometry/euclidean/angle/unoriented/right_angle): lemma naming consistency (#17273)

jsm28 committed 3 years ago

c59f2612

chore(algebra/invertible): weaken typeclass requirements for `invertible.of_left_inverse` (#17267)

eric-wieser committed 3 years ago

ef5d936c

feat(analysis/special_functions/trigonometric/arctan): `arctan_eq_arccos`, `arccos_eq_arctan` (#17172)

jsm28 committed 3 years ago

411b67f5

fix imports post merge

kim-em committed 3 years ago

9a1db238

kim-em committed 3 years ago

488f2dfb

Merge remote-tracking branch 'origin/master' into pnat

kim-em committed 3 years ago

0f8aa6a5

fix downstream imports

kim-em committed 3 years ago

55f89285

fix downstream imports

kim-em committed 3 years ago

6ae95dd5

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

leanprover-community-bot committed 3 years ago

22fe10de

chore(analysis/*): remove some non-terminal simps (#17346)

mcdoll committed 3 years ago

97265543

chore(linear_algebra/finsupp): golf `finsupp.lcongr_symm` (#17341)

eric-wieser committed 3 years ago

83f7236b

kim-em committed 3 years ago

425fb24f

kim-em committed 3 years ago

f93ff044

chore(algebra/order/field): don't import finiteness hierarchy (#17350)

kim-em committed 3 years ago

ef0ef216

kim-em committed 3 years ago

63ed1dbb

kim-em committed 3 years ago

391bcfcc

Merge branch 'split_order_group' into split_order_ring

kim-em committed 3 years ago

c566284e

Merge remote-tracking branch 'origin/master' into split_order_group

kim-em committed 3 years ago

69d99a55

kim-em committed 3 years ago

507e1652

kim-em committed 3 years ago

f275d41f

feat(data/(d)finsupp): well-foundedness of lexicographic and product orders (#16772)

alreadydone committed 3 years ago

e9b8651e

kim-em committed 3 years ago

7533e6fe

add downstream imports

kim-em committed 3 years ago

a5c37779

Newer Older