Commits leanprover-community/mathlib

feat(algebra/big_operators): some lemmas on big operators and `fin` (#7119)

Vierkantor committed 4 years ago

d820a9d7

feat(archive/imo): IMO 1977 Q6 (#7097)

peakpoint committed 4 years ago

8d3e8b5b

feat(order/filter/*, topology/subset_properties): Filter Coprod (#7073)

AlexKontorovich committed 4 years ago

456e5af8

feat(group_theory/perm/cycle_type): Cycle type of a permutation (#6999)

awainverse committed 4 years ago

89196b20

feat(order/ideal, order/pfilter, order/prime_ideal): added `ideal_inter_nonempty`, proved that a maximal ideal is prime (#6924)

atarnoam committed 4 years ago

5775ef75

feat(topology/sheaves): Induced map on stalks (#7092)

justus-springer committed 4 years ago

3df0f773

feat(ring_theory/hahn_series): a `finsupp` of Hahn series is a `summable_family` (#7091)

awainverse committed 4 years ago

98c483b9

chore(algebra/direct_sum_graded): golf proofs (#7029)

gnprice committed 4 years ago

f444128f

feat(archive/100-theorems-list): add proof of Heron's formula (#6989)

matt-kempster committed 4 years ago

3379f3ed

feat(geometry/manifold/instances/units_of_normed_algebra): the units of a normed algebra are a topological group and a smooth manifold (#6981)

Nicknamen committed 4 years ago

27157699

feat(algebra/direct_sum_graded): `A 0` is a ring, `A i` is an `A 0`-module, and `direct_sum.of A 0` is a ring_hom (#6851)

eric-wieser committed 4 years ago

e4edf46d

feat(field_theory/separable_degree): introduce the separable degree (#6743)

JakobScholbach committed 4 years ago

24dc4100

feat(topology/topological_fiber_bundle): topological fiber bundle over `[a, b]` is trivial (#6555)

urkud committed 4 years ago

f12575e8

hack(ci): run lean make twice (#7192)

gebner committed 4 years ago

b3eabc16

WIP: the monoidal and braided structures

kim-em committed 4 years ago

1770a883

refactor(*): kill nat multiplication diamonds (#7084)

sgouezel committed 4 years ago

63801552

feat(category/monoidal): Drinfeld center (without monoidal structure)

kim-em committed 4 years ago

8b0ac8da

feat(data/finset/lattice): le_sup_iff and lt_sup_iff (#7182)

agjftucker committed 4 years ago

3ec54df5

feat(algebra/group/hom): `monoid_with_zero_hom.to_monoid_hom_injective` and co. (#7174)

benjamindavidson committed 4 years ago

500301e7

feat(algebraic_geometry): Basic opens form basis of zariski topology (#7152)

justus-springer committed 4 years ago

4d19f5fa

refactor(src/analysis/normed_space/linear_isometry): generalize to semi_normed_group (#7122)

riccardobrasca committed 4 years ago

724f804b

feat(src/set_theory/surreal): add numeric_add and numeric_omega lemmas (#7179)

apurvnakade committed 4 years ago

06f7d3f0

refactor(algebra/group/defs): remove left-right_cancel_comm_monoids (#7134)

adomani committed 4 years ago

46302c70

feat(logic/function/iterate): `f^[n]^[m] = f^[m]^[n]` (#7121)

adomani committed 4 years ago

92d5cab0

chore(data/equiv/basic): add simps attribute to some defs (#7137)

jcommelin committed 4 years ago

2af01474

feat(data/zsqrtd/basic): add coe_int_dvd_iff lemma (#7161)

Ruben-VandeVelde committed 4 years ago

a1c2bb7d

chore(data/matrix/basic): lemmas for `minor` about `diagonal`, `one`, and `mul` (#7133)

eric-wieser committed 4 years ago

16e2c6ca

refactor(algebra/big_operators, *): specialize `finset.prod_bij` to `fintype.prod_equiv` (#7109)

Vierkantor committed 4 years ago

f9c787da

feat(category_theory/subobject/factor_thru): lemmas in a preadditive category (#7104)

kim-em committed 4 years ago

001628b8

feat(finset/lattice): sup' is to sup as max' is to max (#7087)

agjftucker committed 4 years ago

68e894dc