leanprover-community/mathlib

Pull Requests Commits

introduce old_structure_cmd in group_theory/group_action/defs

adomani committed 4 years ago

70e1ddf2

feat(ring_theory/hahn_series): algebra structure, equivalences with power series (#6540)

awainverse committed 4 years ago

e221dc9a

feat(category_theory/triangulated/basic): add definitions of additive category and triangle (#6539)

l-kershaw committed 4 years ago

eaa02185

feat(normed_group): tendsto_at_top (#6525)

kim-em committed 4 years ago

a7f1e3c6

feat(linear_algebra/matrix): to_matrix and to_lin as alg_equiv (#6496)

pechersky committed 4 years ago

ccd35db8

feat(nat/digits): natural basis representation using list sum and map (#5975)

RaitoBezarius committed 4 years ago

b1ecc987

feat(ring_theory/ideal/operations): add quotient_equiv (#6492)

riccardobrasca committed 4 years ago

fad44b9f

feat(topology): shrinking lemma (#6478)

urkud committed 4 years ago

4e370b5d

feat(number_theory/bernoulli): bernoulli_power_series (#6456)

mo271 committed 4 years ago

05d3955a

feat(linear_algebra): linear_independent_fin_snoc (#6455)

kim-em committed 4 years ago

c9628717

refactor(ring_theory/power_series/basic): simplify truncation (#6605)

gebner committed 4 years ago

b697e523

feat(ring_theory/witt_vector): use structure instead of irreducible (#6604)

gebner committed 4 years ago

09a505a7

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

urkud committed 4 years ago

18d4e519

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

gebner committed 4 years ago

fb674e1e

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

gebner committed 4 years ago

be6753ca

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

urkud committed 4 years ago

366a23fb

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

riccardobrasca committed 4 years ago

9ff74582

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

eric-wieser committed 4 years ago

8e246cbb

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

Vierkantor committed 4 years ago

5d82d1d4

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

urkud committed 4 years ago

3d752421

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

urkud committed 4 years ago

78af5b16

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

adomani committed 4 years ago

792e4921

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

fpvandoorn committed 4 years ago

8713c0bd

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

eric-wieser committed 4 years ago

c1a7c195

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

benjamindavidson committed 4 years ago

fa28a8c5

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

mo271 committed 4 years ago

49afae5a

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

urkud committed 4 years ago

98895022

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

jcommelin committed 4 years ago

a3311136

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

urkud committed 4 years ago

6dec23b2

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

kim-em committed 4 years ago

32bd00f1

Older