leanprover-community/mathlib

Pull Requests Commits

adomani committed 3 years ago

383b18f2

adomani committed 3 years ago

9af9d444

Merge branch 'adomani_covariant_plus' of ssh://github.com/leanprover-community/mathlib into adomani_covariant_plus

adomani committed 3 years ago

695326ae

Merge branch 'master' into adomani_covariant_plus

adomani committed 3 years ago

418762e2

adomani committed 3 years ago

de7a671a

fix(algebra/category/Module/colimits): Add some additional instances with permuted universe parameters (#11812)

adamtopaz committed 3 years ago

553cb9cc

chore(*): use le_rfl instead of le_refl _ (#11797)

jcommelin committed 3 years ago

4cfc30e3

feat(linear_algebra/lagrange): Add recurrence formula for Lagrange polynomials (#11762)

shingtaklam1324 committed 3 years ago

6dcad021

feat(topology/algebra): Inf and inducing preserve compatibility with algebraic structure (#11720)

ADedecker committed 3 years ago

853192ce

fix(algebra/category/Module/colimits): generalize universes (#11802)

jcommelin committed 3 years ago

30a731ca

feat(polynomial/cyclotomic): irreducible cyclotomic polynomials are minimal polynomials (#11796)

ericrbg committed 3 years ago

f2be0d22

feat(data/finset/sort): an order embedding from fin (#11800)

dwarn committed 3 years ago

2c5f36c4

fix(topology/connected): typos in docstrings (#11798)

fpvandoorn committed 3 years ago

25f0406d

feat(algebra/group_power/order): add pow_bit0_pos_iff (#11785)

Ruben-VandeVelde committed 3 years ago

a4d9581e

feat(field_theory/krull_topology): defined Krull topology on Galois groups (#11780)

Sebastian-Monnet committed 3 years ago

324d845a

chore(data/polynomial/monic): dedup `degree_map` (#11792)

ericrbg committed 3 years ago

d6e1c554

feat(set_theory/principal): Principal ordinals are unbounded (#11755)

vihdzp committed 3 years ago

2f4f8ad4

feat(ring_theory/roots_of_unity): coe_injective (#11793)

ericrbg committed 3 years ago

50ee3d56

feat(field_theory/is_alg_closed/classification): Classify algebraically closed fields (#9370)

ChrisHughes24 committed 3 years ago

934f1828

feat(category_theory/linear): compatibility of linear Yoneda (#11784)

TwoFX committed 3 years ago

e39f617c

chore(category_theory/limits): dualize strong_epi (#11783)

TwoFX committed 3 years ago

e61ce5dc

feat(topology/algebra/ordered/monotone_convergence): add `antitone.{ge,le}_of_tendsto` (#11754)

ecstatic-morse committed 3 years ago

93f2bdc8

feat(topology/algebra/group): continuity of action of a group on its own coset space (#11772)

hrmacbeth committed 3 years ago

a4831583

Apply suggestions from code review

adomani committed 3 years ago

Verified d32ac074

chore(*): golf `by_contra, push_neg` to `by_contra'` (#11768)

vihdzp committed 3 years ago

18163786

feat(field_theory/laurent): Laurent expansions of rational functions (#11199)

pechersky committed 3 years ago

89a3c072

feat(field_theory/minpoly): add a nontriviality lemma (#11781)

ericrbg committed 3 years ago

7f3590b4

feat(tactic/equiv_rw): enhancing 'equiv_rw' (#11730)

arthurpaulino committed 3 years ago

cdad1104

add file algebra/order/monoid_lemmas_pos

adomani committed 3 years ago

6af146e2

feat(number_theory): von Mangoldt function (#11727)

b-mehta committed 3 years ago

41811cdd

Older