leanprover-community/mathlib

Pull Requests Commits

ADedecker committed 3 years ago

7e476115

feat(algebra/order/ring): lt_mul_{left,right,self} (#15848)

pechersky committed 3 years ago

d5344df1

feat(topology/algebra/module/basic): continuous versions of `linear_map.comp_sub` and variants (#15870)

ADedecker committed 3 years ago

d1795d68

feat(algebraic_geometry/open_immersion): Restricting a morphism twice is isomorphic to one restriction. (#15710)

erdOne committed 3 years ago

68cc6138

feat(set_theory/game/nim): lemmas about `nim 1` (#14787)

vihdzp committed 3 years ago

2ddf74ab

feat(set_theory/game/nim): Grundy value in terms of right moves (#15410)

vihdzp committed 3 years ago

666c6e00

fix(probability/notation): add missing spaces around operators in notation (#15862)

eric-wieser committed 3 years ago

162413fa

chore(data/seq/*): trivial spacing fixes (#15847)

vihdzp committed 3 years ago

6120aac4

feat(data/real/ennreal): add instance linear_ordered_comm_monoid_with_zero ℝ≥0∞ (#15851)

j-loreaux committed 3 years ago

11cace15

chore(analysis/mean_inequalities_pow): weaken assumptions on rpow_add_le_rpow (#15823)

ericrbg committed 3 years ago

7eaf3412

feat(field_theory/splitting_field): If an intermediate field contains all of the roots, then the polynomial splits (#15658)

tb65536 committed 3 years ago

20f68fc8

feat(number_theory): [S/P^e : R/p] = e * [S/P : R/p], where e is ramification index (#15316)

Vierkantor committed 3 years ago

4d59d4af

feat(category_theory/limits): has_limit F ↔ has_terminal (cone F) (#15797)

TwoFX committed 3 years ago

5424d3f4

feat(topology/continuous_function/basic): inverse equations for `homeomorph.to_continuous_map` (#15708)

ralvrz committed 3 years ago

4f3245c3

chore(data/seq/seq): use `terminates` predicate in `to_list_or_stream` (#15826)

vihdzp committed 3 years ago

0ba3098a

chore(algebra/big_operators): reorder the definitions in `norm_num` extension (#15840)

Vierkantor committed 3 years ago

131c39a4

feat(tactic/field_simp): extend `field_simp` to partial division and units (#14897)

Jon Eugster committed 3 years ago

24a09b31

chore(set_theory/surreal/basic): golf an instance (#15838)

eric-wieser committed 3 years ago

acc7dfa5

chore(analysis/convex/cone): set_like instance (#15715)

eric-wieser committed 3 years ago

c5e83e00

chore(data/seq/seq): clean up spacing (#15825)

vihdzp committed 3 years ago

dd6f53d8

feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. (#15036)

linesthatinterlace committed 3 years ago

1563242e

feat(data/finsupp/basic): `alist.lookup` as a finitely supported function (#15443)

vihdzp committed 3 years ago

637b58e8

refactor(linear_algebra): morphism refactor for `linear_equiv`, `continuous_linear_equiv`, `linear_isometry` and `linear_isometry_equiv` (#15078)

dupuisf committed 3 years ago

798b4ae1

feat(data/seq/seq): improve `cons` and `tail` def-eqs (#15829)

vihdzp committed 3 years ago

078cd612

feat(data/list/basic): `l.nth l.length = none` (#15828)

vihdzp committed 3 years ago

0e87ef97

chore(data/stream/defs): remove match from `stream.cons` (#15789)

pechersky committed 3 years ago

54c4c222

feat(set_theory/ordinal/arithmetic): generalize `mod_opow_log_lt_self` (#15448)

vihdzp committed 3 years ago

53ab3a54

refactor(set_theory/game/nim): remove `nim` namespace (#15366)

vihdzp committed 3 years ago

997fa572

doc(data/polynomial/basic): fix docstring (#15814)

astrainfinita committed 3 years ago

adc4ebc7

chore(probability/martingale): add some parity lemmas for martingales and supermartingales (#15811)

kex-y committed 3 years ago

777082da

Older