leanprover-community/mathlib

Pull Requests Commits

doc(field_theory/galois): add comment that separable extensions are a… (#10500)

kbuzzard committed 4 years ago

2ed7c0ff

refactor(data/nat/fib): use `nat.iterate` (#10489)

urkud committed 4 years ago

fcbe7142

feat(number_theory/padics/padic_norm): prime powers in divisors (#10481)

ericrbg committed 4 years ago

b849b3c2

feat(order/locally_finite): `with_top α`/`with_bot α` are locally finite orders (#10202)

YaelDillies committed 4 years ago

957fa4bb

feat(*/is_R_or_C): deduplicate (#10522)

hrmacbeth committed 4 years ago

202ca0b1

feat(data/int/basic): `nat_abs_dvd_iff_dvd` (#10469)

ericrbg committed 4 years ago

a53da16c

chore(category_theory/limits/shapes/wide_pullbacks): speed up `wide_cospan` (#10535)

pechersky committed 4 years ago

50cc57be

chore(algebra/group_power): golf a few proofs (#10498)

urkud committed 4 years ago

16daabf7

chore(logic): allow `Sort*` args in 2 lemmas (#10517)

urkud committed 4 years ago

77ba0c41

chore(order): generalize `min_top_left` (#10486)

pechersky committed 4 years ago

c058607c

feat(tactic/lint/misc): unused arguments checks for more sorry's (#10431)

fpvandoorn committed 4 years ago

43519fc7

chore(algebra/opposites): split out lemmas about rings and groups (#10457)

eric-wieser committed 4 years ago

dfa98e0e

chore(data/nat/prime): `fact (2.prime)` (#10441)

ericrbg committed 4 years ago

f684721d

chore(algebraic_topology/cech_nerve): An attempt to speed up the proofs... (#10521)

adamtopaz committed 4 years ago

a2e6bf89

chore(analysis/normed_space/hahn_banach): remove `norm'` (#10527)

hrmacbeth committed 4 years ago

044f5320

feat(data/nat/prime): lemma eq_of_eq_count_factors (#10493)

stuart-presnell committed 4 years ago

099fb0f6

feat(data/nat/prime): lemma count_factors_mul_of_coprime (#10492)

stuart-presnell committed 4 years ago

45d45ef0

feat(group_theory/group_action/units): add a `mul_distrib_mul_action` instance (#10480)

eric-wieser committed 4 years ago

b1f90678

feat(category_theory/sites/whiskering): Functors between sheaf categories induced by compositiion (#10496)

adamtopaz committed 4 years ago

b8af4914

feat(topology/algebra/matrix): the determinant is a continuous map (#10503)

ocfnash committed 4 years ago

fcb37903

feat(ring_theory/euclidean_domain): generalize lemmas to PIDs (#10324)

Ruben-VandeVelde committed 4 years ago

d36a67c7

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

leanprover-community-bot committed 4 years ago

150b2179

feat(group_theory/order_of_element): linear ordered rings (#10473)

ericrbg committed 4 years ago

7a19aa1d

Adding a matching TODO back (#10506)

arthurpaulino committed 4 years ago

7348f1b7

refactor(combinatorics/simple_graph): use subgraphs to represent matchings (#10210)

arthurpaulino committed 4 years ago

deb56921

chore(algebra/module/pi): split out `group_theory/group_action/pi` to match `group_theory/group_action/prod` (#10485)

eric-wieser committed 4 years ago

dabb58bb

feat(ring_theory/ideal/operations): add lemmas about comap (#10418)

eric-wieser committed 4 years ago

ea52ec1f

feat(algebra/lie): implement `set_like` for `lie_submodule` (#10488)

Vierkantor committed 4 years ago

9cfa33a6

feat(category_theory/adjunction/whiskering): Whiskering adjunctions. (#10495)

adamtopaz committed 4 years ago

83bce9f1

feat(topology/algebra/[X]): sub[X] of a topological [X] is itself a topological [X] (#10491)

ADedecker committed 4 years ago

61e8aa81

Newer Older