leanprover-community/mathlib3

Pull Requests Commits

feat(data/complex/module): transfer all `has_scalar ℝ` structures to `ℂ` (#6562)

eric-wieser committed 4 years ago

547bf551

feat(ring_theory/valuation/basic): additive valuations (#6559)

awainverse committed 4 years ago

60e25799

feat(linear_algebra/determinant): determinant of a block triangular matrix (#6050)

paulvanwamelen committed 4 years ago

e62a406b

chore(topology/algebra/ordered): add some `at_bot` versions of lemmas (#6618)

urkud committed 4 years ago

664feede

feat(data/real/{nnreal,ennreal}): add (e)nnreal.of_real_bit0/bit1 (#6617)

RemyDegenne committed 4 years ago

f675a864

feat(data/local_equiv,topology/local_homeomorph): add `local_equiv.pi` and `local_homeomorph.pi` (#6574)

urkud committed 4 years ago

df1337ef

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

Newer Older