leanprover-community/mathlib

Pull Requests Commits

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

awainverse committed 3 years ago

478d511e

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

awainverse committed 3 years ago

6b3b6479

awainverse committed 3 years ago

176bac00

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

feat(order/rel_classes): Unbundled typeclass to state that two relations are the non strict and strict versions (#11381)

YaelDillies committed 3 years ago

cd1d839a

refactor(ring_theory): clean up `algebraic_iff_integral` (#11773)

Vierkantor committed 3 years ago

d0027691

Newer Older