leanprover-community/mathlib

Pull Requests Commits

chore(algebra/ring/basic): weaken ring.inverse to only require monoid_with_zero (#6603)

urkud committed 5 years ago

18d4e519

feat(data/finset/lattice): map_sup, map_inf (#6601)

gebner committed 5 years ago

fb674e1e

feat(data/{list,multiset,finset}): map_filter (#6600)

gebner committed 5 years ago

be6753ca

feat(topology/constructions): frontier/interior/closure in `X × Y` (#6594)

urkud committed 5 years ago

366a23fb

feat(algebra/group_power/basic): add abs_add_eq_add_abs_iff (#6593)

riccardobrasca committed 5 years ago

9ff74582

refactor(data/mv_polynomial): cleanup equivs (#6589)

eric-wieser committed 5 years ago

8e246cbb

feat(algebra,linear_algebra): `{smul,lmul,lsmul}_injective` (#6588)

Vierkantor committed 5 years ago

5d82d1d4

chore(data/equiv/local_equiv,topology/local_homeomorph): put `source`/`target` to the left in `∩` (#6583)

urkud committed 5 years ago

3d752421

feat(topology): closure in a `pi` space (#6575)

urkud committed 5 years ago

78af5b16

feat(topology/separation): add API for interaction between discrete topology and subsets (#6570)

adomani committed 5 years ago

792e4921

feat(measure/pi): prove extensionality for `measure.pi` (#6304)

fpvandoorn committed 5 years ago

8713c0bd

chore(data/polynomial/basic): add missing is_scalar_tower and smul_comm_class instances (#6592)

eric-wieser committed 5 years ago

c1a7c195

feat(data/nat/parity): even/odd.mul_even/odd (#6584)

benjamindavidson committed 5 years ago

fa28a8c5

feat(number_theory/bernoulli): bernoulli_poly_eval_one (#6581)

mo271 committed 5 years ago

49afae5a

feat(linear_algebra/pi): add `submodule.pi` (#6576)

urkud committed 5 years ago

98895022

feat(analysis/normed_space/normed_group_hom): bounded homs between normed groups (#6375)

jcommelin committed 5 years ago

a3311136

chore(topology/algebra/ordered): use dot notation, golf some proofs (#6595)

urkud committed 5 years ago

6dec23b2

refactor(topology/bounded_continuous_function): structure extending continuous_map (#6521)

kim-em committed 5 years ago

32bd00f1

feat(algebra/continued_fractions) add determinant formula and approximations for error term (#6461)

kappelmann committed 5 years ago

3e5d90d9

feat(linear_algebra): submodules of f.g. free modules are free (#6178)

Vierkantor committed 5 years ago

0afdaab2

chore(topology): add a few simple lemmas (#6580)

urkud committed 5 years ago

cdc222da

feat(linear_algebra/bilinear_form): Existence of orthogonal basis with respect to a bilinear form (#5814)

kex-y committed 5 years ago

87eec0b6

chore(algebra/module/linear_map): add linear_map.to_distrib_mul_action_hom (#6573)

eric-wieser committed 5 years ago

6791ed9b

chore(algebra/monoid_algebra): provide finer-grained levels of structure for less-structured `G`. (#6572)

eric-wieser committed 5 years ago

13d86df6

feat(linear_algebra/{bilinear,quadratic}_form): inherit scalar actions from algebras (#6586)

eric-wieser committed 5 years ago

7058fa61

feat(algebra/algebra/{basic,tower}): add alg_equiv.comap and alg_equiv.restrict_scalars (#6548)

eric-wieser committed 5 years ago

5d0a40f1

feat(algebraic_topology): simplicial objects and simplicial types (#6195)

kim-em committed 5 years ago

b6ed62ca

feat(bounded_continuous_function): coe_sum (#6522)

kim-em committed 5 years ago

f3dbe9f0

feat(data/set/function): three lemmas about maps_to (#6518)

eric-wieser committed 5 years ago

98c6bbc9

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

leanprover-community-bot committed 5 years ago

5b61f07f

Newer Older