leanprover-community/mathlib3

Pull Requests Commits

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

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

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

kim-em committed 3 years ago

ef0ef216

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

alreadydone committed 3 years ago

e9b8651e

chore(data/polynomial/degree): golf a proof (#17322)

urkud committed 3 years ago

59386b20

feat(combinatorics/simple_graph/connectivity): `is_bridge` and cycle characterization (#17306)

kmill committed 3 years ago

d3abacf0

chore(algebra/ne_zero): move the dependencies out (#17177)

digama0 committed 3 years ago

9f78ea86

chore(category_theory/category/preorder): split material on galois connections (#17339)

kim-em committed 3 years ago

d82b8787

chore(ring_theory/ideal/local_ring): split file (#17319)

urkud committed 3 years ago

c1918ac1

chore(algebra/big_operators): golf 2 proofs (#17345)

urkud committed 3 years ago

315e6cdf

refactor(analysis/complex): use Liouville to prove algebraic closedness (#17343)

alreadydone committed 3 years ago

3642cbed

chore(algebra/group_power/basic): reduce imports (#17334)

kim-em committed 3 years ago

f749197b

chore(data/nat/gcd/basic): remove spurious imports (#17333)

kim-em committed 3 years ago

02812da5

feat(group_theory/abelianization): Add `commutator_representatives` (#17312)

tb65536 committed 3 years ago

0f4c9091

feat(analysis/special_functions): the japanese bracket (#16491)

mcdoll committed 3 years ago

c2d9927e

chore(algebra/field/basic): reduce imports (#17331)

kim-em committed 3 years ago

bf3b52da

chore(algebra/regular/basic): split file (#17179)

kim-em committed 3 years ago

acf831c1

feat(algebra/gcd_monoid): extract gcd from multiset/finset (#17316)

alreadydone committed 3 years ago

43cd4142

Revert "chore(data/nat/cast): remove spurious imports"

kim-em committed 3 years ago

ca1b2371

chore(data/nat/cast): remove spurious imports

kim-em committed 3 years ago

d41e9916

feat(measure_theory/measure/measure_space): Add parallel set of lemmas about count (#17245)

kkytola committed 3 years ago

a0381d50

feat(representation_theory/fdRep): Schur's lemma (#13794)

kim-em committed 3 years ago

b9430470

feat(group_theory/index): add 3 lemmas (#17288)

urkud committed 3 years ago

2fc49d57

chore(algebra/order/group/basic): Improve lemma names (#16970)

YaelDillies committed 3 years ago

402f8982

feat(category_theory): nat_trans.equiv_of_comp_fully_faithful (#17304)

joelriou committed 3 years ago

51c07ea9

feat(category_theory/limits/shapes/*): More API around kernel pairs. (#17301)

erdOne committed 3 years ago

f6bab678

Newer Older