leanprover-community/mathlib

Pull Requests Commits

refactor(field_theory|ring_theory|linear_algebra): minpoly A x (#5774)

jcommelin committed 4 years ago

77003ce2

doc(tactic/rewrite): Add an example for assoc_rw (#5799)

eric-wieser committed 4 years ago

725efb18

refactor(algebraic_geometry/prime_spectrum): simplify `comap_id`, `comap_comp` (#5796)

Jesse Michael Han committed 4 years ago

b5e832e2

feat(order/limsup_liminf, order/filter/ennreal): add properties of limsup for ennreal-valued functions (#5746)

RemyDegenne committed 4 years ago

57bc1dab

feat(algebra/lie/basic): results relating Lie algebra morphisms and ideal operations (#5778)

ocfnash committed 4 years ago

66e955e4

doc(data/buffer/parser/basic): fix typo (#5792)

sorawee committed 4 years ago

9381e37d

chore(field_theory/minpoly): meaningful variable names (#5773)

jcommelin committed 4 years ago

8ab1a39d

feat(ring_theory/ideal/operations): add algebra structure on quotient (#5703)

riccardobrasca committed 4 years ago

db617b3c

chore(category_theory/monad): golf and lint monadic adjunctions (#5769)

b-mehta committed 4 years ago

f3d3d046

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

leanprover-community-bot committed 4 years ago

3089b161

feat(data/option/*): pmap and pbind defs and lemmas (#5442)

pechersky committed 4 years ago

2f824aa1

refactor(algebra/monoid_algebra) generalize from group to monoid algebras (#5785)

Julian-Kuelshammer committed 4 years ago

c3639e94

refactor(analysis/calculus/deriv): simpler proof of `differentiable_at.div_const` (#5782)

Jesse Michael Han committed 4 years ago

f29d1c30

hack(manifold): disable subsingleton instances to speed up simp (#5779)

sgouezel committed 4 years ago

83d44a3d

doc(tactic/auto_cases): fix typo (#5784)

sorawee committed 4 years ago

bf46986e

feat(data/set/lattice): add lemmas set.Union_subtype and set.Union_of_singleton_coe (#5691)

adomani committed 4 years ago

289df3a7

chore(topology/metric_space/isometry): a few more lemmas (#5780)

urkud committed 4 years ago

2c4a5161

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

leanprover-community-bot committed 4 years ago

00e1f4c8

chore(group_theory/perm/{sign,cycles}): renaming for dot notation, linting, formatting (#5777)

bryangingechen committed 4 years ago

dec44fe7

chore(field_theory|ring_theory|linear_algebra): rename minimal_polynomial to minpoly (#5771)

jcommelin committed 4 years ago

a2630fc3

feat(category_theory/is_filtered): is_filtered_of_equiv (#5485)

kl-i committed 4 years ago

0cc93a13

feat(measure_theory/haar_measure): Prove uniqueness (#5663)

fpvandoorn committed 4 years ago

787e6b30

chore(category_theory/limits): coproduct functor (#5677)

b-mehta committed 4 years ago

23373d15

refactor(data/nat/fib): explicitly state fibonacci sequence is monotone (#5776)

Julian-Kuelshammer committed 4 years ago

e0f4142e

refactor(linear_algebra/dual): replace dim<omega by finite_dimensional (#5775)

Julian-Kuelshammer committed 4 years ago

41556652

feat(category_theory/adjunction): reflective functors (#5680)

b-mehta committed 4 years ago

d23dbfba

feat(category_theory/sites): closed sieves (#5282)

b-mehta committed 4 years ago

64abe5aa

chore(topology/metric_space/gluing): use `⨅` notation (#5772)

urkud committed 4 years ago

e076a9c1

feat(linear_algebra/basic): add comap span lemmas (#5744)

ocfnash committed 4 years ago

ba5d1f63

feat(algebraic_geometry/prime_spectrum): add lemma zero_locus_bUnion (#5692)

adomani committed 4 years ago

bd578040

Newer Older