leanprover-community/mathlib3

Pull Requests Commits

hrmacbeth committed 5 years ago

e1d925f4

Cauchy-Riemann equations

hrmacbeth committed 5 years ago

f733acb4

differentiability of re and im

hrmacbeth committed 5 years ago

ae4ce5da

feat(analysis): seminorms and local convexity (#4827)

jlpaca committed 5 years ago

05822370

feat(ring_theory/gauss_lemma): two primitive polynomials divide iff they do in a fraction field (#5003)

awainverse committed 5 years ago

633c2a63

feat(data/nat/choose/sum): alternating binomial coefficient sums (#4997)

awainverse committed 5 years ago

00924146

feat(measure_theory/lp_space): Define Lp spaces (#4993)

RemyDegenne committed 5 years ago

9b887d51

feat(ring_theory/power_basis): `equiv`s between algebras with the same power basis (#4986)

Vierkantor committed 5 years ago

70ca6fd8

feat(category_theory/limits/preserves): functor product preserves colims (#4941)

b-mehta committed 5 years ago

6bac8992

feat(category_theory/equivalence): equivalence of functor categories (#4940)

b-mehta committed 5 years ago

154d73dc

feat(category_theory/limits/creates): transfer creating limits through nat iso (#4938)

b-mehta committed 5 years ago

a0341a89

feat(ring_theory/ideal_operations): prime avoidance (#773)

kckennylau committed 5 years ago

ccc1431c

feat(algebra/squarefree): Defines squarefreeness, proves several equivalences (#4981)

awainverse committed 5 years ago

5f151043

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

leanprover-community-bot committed 5 years ago

4db26afe

feat(tactic/has_variable_names): add tactic for type-based naming (#4988)

JLimperg committed 5 years ago

9ed9e0f8

feat(field_theory/adjoin): Adjoin integral element (#4831)

tb65536 committed 5 years ago

050b8370

feat(ring_theory/unique_factorization_domain): connecting `multiplicity` to `unique_factorization_domain.factors` (#4980)

awainverse committed 5 years ago

eeb20575

feat(analysis/calculus): derivative is measurable (#4974)

sgouezel committed 5 years ago

1a233e0e

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

leanprover-community-bot committed 5 years ago

140d8b42

feat(archive/imo): formalize IMO 1964 problem 1 (#4935)

kbuzzard committed 5 years ago

6b3a2d1d

chore(deprecated/group): Do not import `deprecated` from `equiv/mul_add` (#4989)

eric-wieser committed 5 years ago

6e64df5f

chore(algebra/direct_limit): Use bundled morphisms (#4964)

eric-wieser committed 5 years ago

97a7f577

feat(group_theory/sub{monoid,group}): Add `closure_induction'` for subtypes (#4984)

eric-wieser committed 5 years ago

34215fc9

feat(algebra/pointwise): lemmas relating to submonoids (#4960)

fpvandoorn committed 5 years ago

7404f0ea

feat(algebra/quandle): Bundle `rack.to_envel_group.map` into an equiv (#4978)

eric-wieser committed 5 years ago

593013df

feat(group_theory/subgroup) top is a normal subgroup (#4982)

alexjbest committed 5 years ago

3f575d72

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

leanprover-community-bot committed 5 years ago

509a2242

feat(algebra/group/with_one): Use an equiv for `lift` (#4975)

eric-wieser committed 5 years ago

f6c8d81c

feat(data/matrix): little lemmas on `map` (#4874)

Vierkantor committed 5 years ago

49cf28fe

refactor(group_theory/group_action): Break the file into three pieces (#4936)

eric-wieser committed 5 years ago

67309a44

Older