leanprover-community/mathlib3

Pull Requests Commits

feat(analysis): prove that a polynomial function is equivalent to its leading term along at_top, and consequences (#5354)

ADedecker committed 4 years ago

5d4d8158

refactor(measure_theory/ae_eq_fun): move emetric to `ae_eq_fun_metric` (#6081)

sgouezel committed 4 years ago

99fe12af

chore(measure_theory/measure_space): move definition of `measure.ae` up (#6051)

urkud committed 4 years ago

5a25827e

fix(scripts): make lint-style.* work on macos and windows (#6047)

Julian committed 4 years ago

132b0fe9

feat(logic/function/basic): add lemma stating that dite of two injective functions is injective if images are disjoint (#5866)

agusakov committed 4 years ago

288cc2e4

refactor(analysis/calculus/mean_value): use `is_R_or_C` in more lemmas (#6022)

urkud committed 4 years ago

c25dad98

feat(ring_theory/polynomial): Almost Vieta's formula on products of (X + r) (#5696)

winston-h-zhang committed 4 years ago

8b1f3237

refactor(analysis/normed_space): upgrade `linear_map.to_continuous_linear_map` to `linear_equiv` (#6072)

urkud committed 4 years ago

4b035fcd

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

leanprover-community-bot committed 4 years ago

736929e5

feat(algebra/group/hom): add inv_comp and comp_inv (#6046)

kbuzzard committed 4 years ago

7f467fad

feat(algebra/ordered_ring): add lemma (#6031)

adomani committed 4 years ago

7c53a168

feat(category_theory): connected components of a category (#5425)

b-mehta committed 4 years ago

7ec4fcc3

refactor(data/buffer/parser/basic): make valid a class and rename to mono (#6015)

pechersky committed 4 years ago

a1ebf540

feat(topology/category): constructor for compact hausdorff spaces (#6068)

b-mehta committed 4 years ago

dbf038d6

refactor(topology): make two definitions irreducible from the start (#6060)

sgouezel committed 4 years ago

767e6ae0

doc(number_theory/*): provide docstrings for basic and dioph (#6063)

Julian-Kuelshammer committed 4 years ago

2bdeda9c

feat(data/nat): division of powers (#6067)

b-mehta committed 4 years ago

d951b2b4

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

leanprover-community-bot committed 4 years ago

b8a6f811

fix(ring_theory/power_series/basic): fix algebra arguments (#6065)

eric-wieser committed 4 years ago

b6b90e28

feat(data/list/basic): simp iffs about *fix nil (#6064)

pechersky committed 4 years ago

94033d8e

feat(algebra/star): star_ordered_ring (#4685)

kim-em committed 4 years ago

0926e674

chore(linear_algebra): move `is_basis_std_basis` to `std_basis.lean` (#6054)

Vierkantor committed 4 years ago

bd38c5ff

feat(data/nat/factorial): non-strict inequality on factorial (#6052)

adomani committed 4 years ago

b5c23cea

feat(algebra/ordered_ring): proof that `a + b ≤ a * b` (#6043)

adomani committed 4 years ago

1ab7cf67

feat(algebra/char_zero): add char_zero lemma for ordered_semirings (#6038)

adomani committed 4 years ago

fa9bf621

feat(linear_algebra/multilinear): add more `curry` equivs (#6012)

urkud committed 4 years ago

c2c686e4

feat(linear_algebra/projection): Extending maps from complement submodules to the entire module (#5981)

kex-y committed 4 years ago

dc985478

refactor(*): remove uses of @[class] def (#6028)

digama0 committed 4 years ago

34e366c6

refactor(topology/algebra/module,analysis/*): merge some `smul` lemmas and defs (#5987)

urkud committed 4 years ago

c6c7eaf3

chore(algebra/algebra/basic): show that the ℚ-algebra structure is unique (#5980)

eric-wieser committed 4 years ago

392ebecd

Newer Older