leanprover-community/mathlib

Pull Requests Commits

chore(*): split lines and move module doc `measure_theory/category/Meas` (#6459)

Julian-Kuelshammer committed 5 years ago

aa0b274b

feat(ring_theory/power_series/basic): coeff_zero_X_mul (#6445)

mo271 committed 5 years ago

d1b7a676

feat(data/option): add `option.forall` and `option.exists` (#6419)

urkud committed 5 years ago

a19af600

feat(tactic/apply_fun): work on the goal as well (#6439)

kim-em committed 5 years ago

4b02853b

chore(data/nat/choose): fix namespace of theorems (#6451)

kim-em committed 5 years ago

7256361a

feat(ring_theory/power_series/basic): rescale_inj (#6446)

mo271 committed 5 years ago

5f68d0e5

feat(algebra/homology/chain_complex): pushforward of complex w.r.t. additive functor (#6403)

adamtopaz committed 5 years ago

f33418a9

feat(category_theory/skeletal): skeleton of a general category (#6443)

b-mehta committed 5 years ago

7ce01bbc

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

leanprover-community-bot committed 5 years ago

1af882b4

feat(category_theory/monoidal): construct the monoidal inverse to a functor (#6442)

b-mehta committed 5 years ago

d38b5a50

feat(linear_algebra/basic): add is_scalar_tower instance for hom type (#6331)

kbuzzard committed 5 years ago

a225e12c

feat(algebra/lie/solvable): images of solvable Lie algebras are solvable (#6413)

ocfnash committed 5 years ago

407615e0

feat(category_theory/subobject): kernels and images as subobjects (#6301)

kim-em committed 5 years ago

ddefd965

feat(data/equiv/basic): Add `fin_succ_above_equiv` (#5145)

eric-wieser committed 5 years ago

11e1cc36

feat(linear_algebra/tensor_product): allow different semirings in linear_map.flip (#6414)

eric-wieser committed 5 years ago

20b49fbd

feat(algebra/big_operators): add lemmas about `sum` and `pi.single` (#6390)

urkud committed 5 years ago

47b62ea4

feat(topology/instances/real, topology/metric_space/basic, algebra/floor): integers are a proper space (#6437)

hrmacbeth committed 5 years ago

aeda3fb7

chore(data/finsupp/basic): add coe_{neg,sub,smul} lemmas to match coe_{zero,add,fn_sum} (#6350)

eric-wieser committed 5 years ago

ff5fa529

feat(algebraic_topology): introduce the simplex category (#6173)

kim-em committed 5 years ago

dd5363b5

feat(polynomial/eval): lemmas relating eval/map on numerals (#6438)

kim-em committed 5 years ago

2f1de3f7

feat(analysis/complex/basic): complex conjugation is a linear isometry (#6436)

hrmacbeth committed 5 years ago

300e81de

feat(data/polynomial): basic lemmas (#6434)

kim-em committed 5 years ago

274042d5

feat(data/polynomial/degree/trailing_degree): Trailing degree of multiplication by X^n (#6425)

tb65536 committed 5 years ago

cca22d7b

feat(algebra/category/Semigroup/basic): categories of magmas and semigroups (#6387)

Julian-Kuelshammer committed 5 years ago

24ed74a2

feat(ring_theory/flat): definition of flat module (#6284)

jcommelin committed 5 years ago

aafa5fe4

doc(data/finset/basic): rewrite finset module doc (#5893)

winston-h-zhang committed 5 years ago

d451876b

feat(algebra/algebra/basic): smul_mul_smul (#6423)

tb65536 committed 5 years ago

07d6d3f1

chore(*): upgrade to Lean 3.27.0c (#6411)

robertylewis committed 5 years ago

0035e2dd

fix(logic/{function}/basic): remove simp lemmas `function.injective.eq_iff` and `imp_iff_right` (#6402)

robertylewis committed 5 years ago

5fbebf67

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

leanprover-community-bot committed 5 years ago

09388808

Newer Older