leanprover-community/mathlib3

Pull Requests Commits

Update initial_seg.lean

vihdzp committed 3 years ago

7c2d0580

Update initial_seg.lean

vihdzp committed 3 years ago

9575707f

Merge branch 'inl_initial_seg' into initial_seg_golf

vihdzp committed 3 years ago

ea112c67

Update initial_seg.lean

vihdzp committed 3 years ago

a879c9d4

Update initial_seg.lean

vihdzp committed 3 years ago

d402a6b6

Merge branch 'rel_embedding_empty' into initial_seg_golf

vihdzp committed 3 years ago

3402608c

Update rel_iso.lean

vihdzp committed 3 years ago

7a4c7d2e

Update arithmetic.lean

vihdzp committed 3 years ago

80146393

Update initial_seg.lean

vihdzp committed 3 years ago

61a6fd0a

Update initial_seg.lean

vihdzp committed 3 years ago

5ab6da87

vihdzp committed 3 years ago

e59170b1

Merge branch 'rel_embedding_inl' into inl_initial_seg

vihdzp committed 3 years ago

f5f7d17b

Merge branch 'principal_seg_move' into inl_initial_seg

vihdzp committed 3 years ago

f0906038

doc(logic/equiv/basic): explicitly state functions equivalences are based on (#15354)

vihdzp committed 3 years ago

635b8585

feat(analysis/asymptotics/asymptotics): generalize, golf (#15010)

urkud committed 3 years ago

466b8922

golf(data/polynomial/degree/definitions): golf three proofs (#15236)

adomani committed 3 years ago

356f889c

feat(ring_theory/integrally_closed): if x is in Frac R such that x^n is in R then x is in R (#12812)

Multramate committed 3 years ago

0bea64b5

Update rel_iso.lean

vihdzp committed 3 years ago

11e0ddd9

Update rel_iso.lean

vihdzp committed 3 years ago

77ce9129

feat(data/fin/basic): add a reflected instance (#15337)

eric-wieser committed 3 years ago

f3fac409

chore(*): upgrade to lean 3.45.0c (#15325)

eric-wieser committed 3 years ago

48b7ad6f

feat(algebra/module/linear_map): use morphisms class for lemmas about linear [pre]images of `c • S` (#15103)

ADedecker committed 3 years ago

51f5e6cc

Update initial_seg.lean

vihdzp committed 3 years ago

b845ce4e

feat(measure_theory/integral/set_integral): add `set_integral_indicator` (#15344)

kex-y committed 3 years ago

25706131

feat(measure_theory/constructions/prod): The layercake integral. (#14424)

kkytola committed 3 years ago

f3ae2d0d

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

erdOne committed 3 years ago

073c3ace

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

leanprover-community-bot committed 3 years ago

e479bfbe

vihdzp committed 3 years ago

11451068

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

Older