leanprover-community/mathlib3

Pull Requests Commits

chore(algebra/group_power): generalize `semiring` version of Bernoulli's inequality (#5831)

urkud committed 5 years ago

faba9cea

feat(measure_theory/interval_integral) : add integration by parts (#5724)

mmasdeu committed 5 years ago

0feb1d20

feat(order/modular_lattice): define modular lattices (#5564)

awainverse committed 5 years ago

de10203f

chore(data/nat/basic): reuse a proof, drop a duplicate (#5836)

urkud committed 5 years ago

38ae9b37

feat(data/polynomial/algebra_map): aeval_map (#5843)

tb65536 committed 5 years ago

8b4c455b

feat(field_theory/minpoly): Minimal polynomials of degree one (#5844)

tb65536 committed 5 years ago

bef50a4d

feat(topology/metric_space/{basic,emetric_space}): product of balls of the same size (#5846)

urkud committed 5 years ago

6958d8cd

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

leanprover-community-bot committed 5 years ago

244b3ed0

chore(analysis/analytic/composition): minor golfing (#5839)

urkud committed 5 years ago

c681f48c

feat(computability/language): le on languages (#5704)

foxthomson committed 5 years ago

228c00ba

chore(algebra/group_power): add `(a+b)^2=a^2+2ab+b^2` (#5838)

urkud committed 5 years ago

b2ca7614

fix(tactic/default): make field_simp work with import tactic (#5832)

bryangingechen committed 5 years ago

fac0f253

feat(algebra/lie/basic): show `I + J` is solvable if Lie ideals `I`, `J` are solvable (#5819)

ocfnash committed 5 years ago

b52b3041

fix(group_theory/group_action/defs): fix minor typo (#5827)

Julian-Kuelshammer committed 5 years ago

3ef82811

chore(algebra/group/conj): move `conj_injective` and use existing proofs (#5798)

eric-wieser committed 5 years ago

b3a21123

feat(measure_theory/interval_integral): FTC-2 for the open set (#5733)

benjamindavidson committed 5 years ago

d66d5639

feat(ring_theory/polynomial): symmetric polynomials and elementary symmetric polynomials (#5788)

winston-h-zhang committed 5 years ago

ce9bc688

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

leanprover-community-bot committed 5 years ago

a19e48b1

feat(data/nat/modeq): Generalised version of the Chinese remainder theorem (#5683)

alexjbest committed 5 years ago

b2d95c0c

feat(field_theory/normal): Splitting field is normal (#5768)

tb65536 committed 5 years ago

8b6f541e

chore(data/list/range): Add range_zero and rename range_concat to range_succ (#5821)

eric-wieser committed 5 years ago

7c892653

chore(data/dfinsupp): add `dfinsupp.prod_comm` (#5817)

eric-wieser committed 5 years ago

2ec396a7

refactor(data/fin): shorter proof of `mk.inj_iff` (#5811)

Jesse Michael Han committed 5 years ago

9cdffe9c

feat(data/list/range): nth_le_fin_range (#5456)

pechersky committed 5 years ago

c700791b

feat(data/fin): add_comm_monoid and simp lemmas (#5010)

pechersky committed 5 years ago

9ae33174

feat(algebraic_geometry/is_open_comap_C): add file is_open_comap_C, prove that Spec R[x] \to Spec R is an open map (#5693)

adomani committed 5 years ago

a7a4f34c

feat(category_theory/monad): algebras for the coproduct monad (#5679)

b-mehta committed 5 years ago

0c57d1e7

feat(char_p/quotient): Add a lemma to inherit char_p from the underlying ring (#5809)

eric-wieser committed 5 years ago

e41b917c

feat(ring_theory/ideal/operations): generalize quotient of algebras (#5802)

riccardobrasca committed 5 years ago

385173df

feat(category_theory/limits): preserve monomorphisms (#5801)

b-mehta committed 5 years ago

31fd5b58

Newer Older