leanprover-community/mathlib3

Pull Requests Commits

feat(data/finset/basic): mem_map_equiv (#6399)

gebner committed 4 years ago

9d748f0b

feat(ring_theory/power_series/basic): remove const coeff (#6383)

mo271 committed 4 years ago

eba9be51

feat(data/zmod/basic): Explicitly state computable right_inverses instead of just surjectivity (#5797)

eric-wieser committed 4 years ago

a31d06a7

feat(data/list/basic): take_init, take_eq_nil (#6380)

pechersky committed 4 years ago

a518fb86

feat(data/mv_polynomial/basic): add two equivs (#6324)

riccardobrasca committed 4 years ago

e66e136f

feat(geometry/manifold): `model_with_corners` is a `closed_embedding` (#6393)

urkud committed 4 years ago

ead4731a

feat(algebra/lie/cartan_subalgebra): define Cartan subalgebras (#6385)

ocfnash committed 4 years ago

27b6110e

feat(data/multiset/basic): subsingleton_equiv_apply' (#6400)

gebner committed 4 years ago

25ea4998

fix(tactic/delta_instance): beta reduce type of instance (#6396)

robertylewis committed 4 years ago

6271fe5b

fix(topology/metric_space/cau_seq_filter): remove non-terminal simp (#6401)

gebner committed 4 years ago

3d9e7907

chore(data/matrix/basic): instances for unique, subsing, nontriv, coe (#6296)

pechersky committed 4 years ago

12afc981

feat(data/complex|matrix): instances of star_ordered_ring and star_ordered_algebra (#4686)

kim-em committed 4 years ago

85636f9a

feat(topology/separation): a cont. function with a cont. left inverse is a closed embedding (#6329)

urkud committed 4 years ago

196c2a8a

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

leanprover-community-bot committed 4 years ago

9bad59cf

fix(data/int/basic,category_theory/equivalence): use neg not minus in lemma names (#6384)

eric-wieser committed 4 years ago

4a391c9d

feat(category_theory/abelian/additive_functor): Adds definition of additive functors (#6367)

adamtopaz committed 4 years ago

358fdf23

chore(data/equiv/local_equiv,topology/local_homeomorph,data/set/function): review (#6306)

urkud committed 4 years ago

b4d2ce45

feat(data/real/sqrt): add continuity attributes (#6388)

benjamindavidson committed 4 years ago

387db0d9

doc(measure_theory/interval_integral): move comment (#6386)

fpvandoorn committed 4 years ago

8cfada11

feat(data/list/basic): nth_drop (#6381)

pechersky committed 4 years ago

2d51a449

chore(group_theory/coset): right_coset additions and module doc (#6371)

Julian-Kuelshammer committed 4 years ago

63e75351

feat(logic/basic): subsingleton_iff_forall_eq (#6379)

kex-y committed 4 years ago

750d117d

feat(algebra/lie/nilpotent): basic facts about nilpotent Lie algebras (#6378)

ocfnash committed 4 years ago

59bf982e

feat(ring_theory/power_series/well_known): sum of power of exponentials (#6368)

mo271 committed 4 years ago

4b22c39d

feat(measure_theory/integration): add theorems about the product of independent random variables (#6106)

mzinkevi committed 4 years ago

e3d6cf82

feat(category_theory/subobject): the semilattice_inf/sup of subobjects (#6278)

kim-em committed 4 years ago

f84f5b2e

feat(chain_complex): lemmas about eq_to_hom (#6250)

kim-em committed 4 years ago

7f46c811

feat(data/buffer/basic): read and to_buffer lemmas (#6048)

pechersky committed 4 years ago

8d3efb71

feat(logic/basic): subsingleton_of_forall_eq (#6376)

kex-y committed 4 years ago

391c90a3

feat(ring_theory/power_series/basic): coeff_succ_X_mul (#6370)

mo271 committed 4 years ago

e6d23d23

Newer Older