leanprover-community/mathlib3

Pull Requests Commits

chore(*): update to lean 3.39.0c (#11821)

gebner committed 3 years ago

cedcf073

feat(group_theory/subgroup/basic): add pi subgroups (#11801)

nomeata committed 3 years ago

049a1b2b

feat(logic/basic): add projection notation for iff (#11803)

fpvandoorn committed 3 years ago

46c48d7f

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

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

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

b-mehta committed 3 years ago

41811cdd

refactor(set_theory/ordinal_arithmetic): Simpler `bsup` definition (#11386)

vihdzp committed 3 years ago

c235c612

feat(topology/connected): Connectedness of unions of sets (#10005)

AntoineChambert-Loir committed 3 years ago

4d0b3983

feat(group_theory/p_group): finite p-groups with different p have coprime orders (#11775)

nomeata committed 3 years ago

d6c002c7

refactor(set_theory/ordinal): Add `covariant_class` instances for ordinal addition and multiplication (#11678)

vihdzp committed 3 years ago

307a456f

Newer Older