leanprover-community/mathlib

Pull Requests Commits

feat(field_theory/polynomial_galois_group): ext lemma (#6627)

tb65536 committed 5 years ago

41f11966

feat(group_theory/solvable): Commutative groups are solvable (#6625)

tb65536 committed 5 years ago

3dd12573

feat(field_theory/splitting_field): splits_pow (#6624)

tb65536 committed 5 years ago

2c4a9855

refactor(topology): make is_closed a class (#6552)

sgouezel committed 5 years ago

653fd292

feat(measure_theory/pi_system) lemmas for pi_system, useful for independence. (#6353)

mzinkevi committed 5 years ago

56065f7e

feat(linear_algebra/basic): add missing lemma finsupp.sum_smul_index_linear_map' (#6565)

ocfnash committed 5 years ago

925ea07d

chore(geometry/manifold): use notation `𝓘(𝕜, E)` (#6636)

urkud committed 5 years ago

b7c5709d

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

leanprover-community-bot committed 5 years ago

514973a9

feat(data/dfinsupp): add is_scalar_tower and smul_comm_class (#6614)

eric-wieser committed 5 years ago

0e321167

ci(.github/workflows/build.yml): do not install azcopy, change upload logic (#6613)

bryangingechen committed 5 years ago

a814e189

chore(ring_theory/polynomial/basic): remove a use of comap (#6612)

eric-wieser committed 5 years ago

c5c97f27

chore(topology/metric/hausdorff_distance): use `infi`/`supr` (#6611)

urkud committed 5 years ago

590444c4

chore(linear_algebra/quadratic_form): clean up universe collisions, generalize smul lemmas (#6609)

eric-wieser committed 5 years ago

5be9ceae

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

eric-wieser committed 5 years ago

547bf551

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

awainverse committed 5 years ago

60e25799

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

paulvanwamelen committed 5 years ago

e62a406b

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

urkud committed 5 years ago

664feede

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

RemyDegenne committed 5 years ago

f675a864

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

urkud committed 5 years ago

df1337ef

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

awainverse committed 5 years ago

e221dc9a

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

l-kershaw committed 5 years ago

eaa02185

feat(normed_group): tendsto_at_top (#6525)

kim-em committed 5 years ago

a7f1e3c6

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

pechersky committed 5 years ago

ccd35db8

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

RaitoBezarius committed 5 years ago

b1ecc987

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

riccardobrasca committed 5 years ago

fad44b9f

feat(topology): shrinking lemma (#6478)

urkud committed 5 years ago

4e370b5d

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

mo271 committed 5 years ago

05d3955a

feat(linear_algebra): linear_independent_fin_snoc (#6455)

kim-em committed 5 years ago

c9628717

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

gebner committed 5 years ago

b697e523

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

gebner committed 5 years ago

09a505a7

Newer Older