leanprover-community/mathlib3

Pull Requests Commits

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

foxthomson committed 4 years ago

228c00ba

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

urkud committed 4 years ago

b2ca7614

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

bryangingechen committed 4 years ago

fac0f253

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

ocfnash committed 4 years ago

b52b3041

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

Julian-Kuelshammer committed 4 years ago

3ef82811

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

eric-wieser committed 4 years ago

b3a21123

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

benjamindavidson committed 4 years ago

d66d5639

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

winston-h-zhang committed 4 years ago

ce9bc688

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

leanprover-community-bot committed 4 years ago

a19e48b1

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

alexjbest committed 4 years ago

b2d95c0c

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

tb65536 committed 4 years ago

8b6f541e

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

eric-wieser committed 4 years ago

7c892653

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

eric-wieser committed 4 years ago

2ec396a7

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

Jesse Michael Han committed 4 years ago

9cdffe9c

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

pechersky committed 4 years ago

c700791b

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

pechersky committed 4 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 4 years ago

a7a4f34c

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

b-mehta committed 4 years ago

0c57d1e7

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

eric-wieser committed 4 years ago

e41b917c

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

riccardobrasca committed 4 years ago

385173df

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

b-mehta committed 4 years ago

31fd5b58

feat(algebra/lie/basic): additional lemmas concerning `lie_algebra.derived_series_of_ideal` (#5815)

ocfnash committed 4 years ago

a3ef65da

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

leanprover-community-bot committed 4 years ago

b1d56736

chore(algebra/group/hom): Add `mk_coe` lemmas (#5812)

eric-wieser committed 4 years ago

d7a8709e

feat(measure_theory/lp_space): extend the definition of Lp seminorm to p ennreal (#5808)

RemyDegenne committed 4 years ago

b1214293

chore(order/filter/basic): add `eventually_eq.rfl` and `eventually_le.rfl` (#5805)

urkud committed 4 years ago

9d14a5f3

feat(analysis/normed_space,topology/metric_space): distance between diagonal vectors (#5803)

urkud committed 4 years ago

21b0b012

feat(data/buffer/parser/numeral): numeral parser defs (#5462)

pechersky committed 4 years ago

da6e3c36

chore(category_theory/adjunction): move reflective functor lemmas (#5800)

b-mehta committed 4 years ago

8b47563e

feat(algebra/lie/basic): generalise the definition of `lie_algebra.derived_series` (#5794)

ocfnash committed 4 years ago

90763c46

Newer Older