leanprover-community/mathlib

Pull Requests Commits

Eric's inf lemmas

adomani committed 3 years ago

23b2c74a

Eric's suggestions

adomani committed 3 years ago

Verified 43bb5da0

adomani committed 3 years ago

1542133c

adomani committed 3 years ago

548449d3

add max_degree_add_le

adomani committed 3 years ago

bb1dfbf3

adomani committed 3 years ago

d63d8867

(trailing_)degree --> min/max_degree

adomani committed 3 years ago

3bca0d89

adomani committed 3 years ago

5418975f

revert to working version

adomani committed 3 years ago

e5b797ee

Revert "Junyan Xu's proof"

adomani committed 3 years ago

440f9ddf

adomani committed 3 years ago

d038dced

Merge branch 'adomani_ama_degree' of ssh://github.com/leanprover-community/mathlib into adomani_ama_degree

adomani committed 3 years ago

a7ceaa01

Merge branch 'master' into adomani_ama_degree

adomani committed 3 years ago

ec2e1b6d

Eric's suggestions

adomani committed 3 years ago

Verified 83de8b24

Revert "Eric's proof"

adomani committed 3 years ago

83681da9

adomani committed 3 years ago

131e6172

adomani committed 3 years ago

df94bd51

feat(ring_theory): Basic framework for classes of ring homomorphisms (#14966)

erdOne committed 3 years ago

073c3ace

Junyan Xu's proof

adomani committed 3 years ago

dc521152

too many lemmas

adomani committed 3 years ago

fb7a2658

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

leanprover-community-bot committed 3 years ago

e479bfbe

chore(set_theory/pgame): remove redundant `dsimp` (#15312)

vihdzp committed 3 years ago

b89df0ab

chore(data/matrix/block): lemmas about swapping blocks of matrices (#15298)

eric-wieser committed 3 years ago

4302cb7e

doc(set_theory/ordinal/cantor_normal_form): document most theorems (#15227)

vihdzp committed 3 years ago

5590b0a2

chore(order/order_iso_nat): remove `decidable_pred` assumption from `subtype.order_iso_of_nat` (#15190)

vihdzp committed 3 years ago

5744b50d

feat(data/finset/basic): Add `decidable_nonempty` for finsets. (#15170)

linesthatinterlace committed 3 years ago

08648056

feat(linear_algebra/projectivization/independence): defines (in)dependence of points in projective space (#14542)

Michael14071407 committed 3 years ago

1e82f5ec

feat(topology/local_homeomorph): "injectivity" local_homeomorph.prod (#15311)

fpvandoorn committed 3 years ago

f7313156

feat(analysis/calculus/cont_diff): extra lemmas about cont_diff_within_at (#15309)

fpvandoorn committed 3 years ago

25f60b46

feat(tactic/linear_combination): add parser for `h / a` (#15284)

digama0 committed 3 years ago

51f76d05

Older