leanprover-community/mathlib

Pull Requests Commits

Merge branch 'multiset_lemmas' into finset_lemmas

vihdzp committed 3 years ago

2a38c710

Update basic.lean

vihdzp committed 3 years ago

24ced788

vihdzp committed 3 years ago

3cd4154b

Merge branch 'multiset_lemmas' into finset_lemmas

vihdzp committed 3 years ago

b93c330a

Merge branch 'multiset_tweaks' into multiset_lemmas

vihdzp committed 3 years ago

228b2781

vihdzp committed 3 years ago

72fdd04f

refactor(analysis/normed_space/operator_norm): generalize `continuous_linear_map.lmul` to non-unital algebras (#15868)

j-loreaux committed 3 years ago

a6b56ec2

feat(measure_theory/function/ae_eq_of_integral): remove a finite_measure assumption (#15899)

sgouezel committed 3 years ago

a97d85de

feat(analysis/normed_space/multilinear): constant scalar multiplication is continuous (#15897)

mcdoll committed 3 years ago

2be2f2cb

doc(linear_algebra/clifford_algebra/basic): docstring clarification (#15892)

kbuzzard committed 3 years ago

9a5b9842

feat(probability/upcrossing): Doob's upcrossing estimate (#14933)

kex-y committed 3 years ago

e2333f32

feat(topology/metric_space/*): `additive`/`multiplicative`/`order_dual` instances (#15704)

YaelDillies committed 3 years ago

14d34b71

feat(data/nat): Add new binary recursors; prove the relationship between `nat.bits` and other pieces of code (#14990)

prakol16 committed 3 years ago

e3d2f74c

vihdzp committed 3 years ago

88448ae1

Update concrete.lean

vihdzp committed 3 years ago

dbac2a06

Update concrete.lean

vihdzp committed 3 years ago

40a2d5ff

feat(order/complete_lattice): add `equiv.supr_congr` and `equiv.supr_comp` lemmas (#15852)

j-loreaux committed 3 years ago

dffc243a

vihdzp committed 3 years ago

50cbeef1

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

pechersky committed 3 years ago

d5344df1

Update basic.lean

vihdzp committed 3 years ago

f82dc4b7

Update nodup.lean

vihdzp committed 3 years ago

f35a74f0

Update basic.lean

vihdzp committed 3 years ago

d913b355

vihdzp committed 3 years ago

80eb6cdc

vihdzp committed 3 years ago

530198b8

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

Older