leanprover-community/mathlib

Pull Requests Commits

chore(analysis/convex/topology): generalize a few lemmas (#13656)

urkud committed 3 years ago

7d64215f

chore(number_theory/padics/*): tidy some proofs (#13652)

Ruben-VandeVelde committed 3 years ago

c24f1f2b

chore(field_theory/finite/polynomial): tidy + remove nolints (#13645)

ericrbg committed 3 years ago

962bfcdb

chore(ring_theory/witt_vector/isocrystal): speed up the proof (#13644)

yuma-mizuno committed 3 years ago

b6a4be44

feat(topology/algebra/matrix): `matrix.block_diagonal` is continuous (#13641)

eric-wieser committed 3 years ago

9c861e32

feat(group_theory/complement): The range of a section `G ⧸ H → G` is a transversal (#13623)

tb65536 committed 3 years ago

b1b2cab4

refactor(group_theory/schur_zassenhaus): Golf proof of abelian case (#13622)

tb65536 committed 3 years ago

6cbf986a

refactor(linear_algebra/quotient): Use the same quotient relation as add_subgroup (#13620)

eric-wieser committed 3 years ago

b6c8c0d4

chore(analysis/normed_space/finite_dimension): extract some lemmas from existentials (#13600)

eric-wieser committed 3 years ago

91b80842

chore(data/matrix): generalisation linter (#13655)

ericrbg committed 3 years ago

070c21b6

refactor(order/ideal): Make `order.ideal` extend `lower_set` (#13070)

YaelDillies committed 3 years ago

df4066cf

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

leanprover-community-bot committed 3 years ago

d4d5b6d2

feat(set_theory/game/pgame): `x.move_left i < x` and variants (#13654)

vihdzp committed 3 years ago

65edf255

chore(topology/metric_space/basic): golf an instance (#13664)

urkud committed 3 years ago

454b8848

docs(number_theory/sum_two_squares): Update docs (#13593)

vihdzp committed 3 years ago

9101c48b

docs(tactic/algebra): Module docstring (#13571)

YaelDillies committed 3 years ago

045fc443

feat(algebra/polynomial/big_operators): add a lemma, reduce assumptions, golf (#13264)

astrainfinita committed 3 years ago

54d1ddd2

refactor(*): migrate from `filter.lift' _ powerset` to `filter.small_sets` (#13673)

urkud committed 3 years ago

0d16bb4d

chore(order/filter/small_sets): redefine, golf (#13672)

urkud committed 3 years ago

53a484e6

feat(data/quot): Decidability of `quotient.lift` and friends (#13589)

YaelDillies committed 3 years ago

42b9cdf8

refactor(linear_algebra/dimension): further generalisations to division_ring (#13657)

kim-em committed 3 years ago

63da426d

feat(set_theory/surreal/basic): Definitional characterization of `numeric` (#13653)

vihdzp committed 3 years ago

81262559

feat(algebra/hom/iterate): Iterating an action (#13659)

tb65536 committed 3 years ago

e006f38c

refactor(category_theory/monoidal): prove coherence lemmas by coherence (#13406)

kim-em committed 3 years ago

b8b8bf3e

feat(set_theory/game/pgame): Birthdays of pre-games (#13636)

vihdzp committed 3 years ago

92ca1369

chore(order/filter/basic): golf 2 proofs (#13614)

urkud committed 3 years ago

5998b497

chore(set_theory/game/pgame): Cleanup (#13612)

vihdzp committed 3 years ago

946f253c

docs(tactic/lint/default): Module docstring (#13570)

YaelDillies committed 3 years ago

b0552c15

chore(algebra/*): move function instances (#13650)

eric-wieser committed 3 years ago

2d0ff329

feat(algebra/ring/basic): generalisation linter suggestions (#13649)

ericrbg committed 3 years ago

cc406db0

Newer Older