leanprover-community/mathlib3

Pull Requests Commits

themathqueen committed 2 years ago

3a150f90

themathqueen committed 2 years ago

cf2106cf

themathqueen committed 2 years ago

0fb02b47

themathqueen committed 2 years ago

213ec182

themathqueen committed 2 years ago

05308bc5

themathqueen committed 2 years ago

8e7a82c7

move non-finitedimensional stuff to other file

themathqueen committed 2 years ago

09ad49a7

added lemmas for clm

themathqueen committed 2 years ago

c5d3db0b

move file to new pr

themathqueen committed 2 years ago

537fc76f

Merge branch 'invariant_submodule' of https://github.com/leanprover-community/mathlib into finite_dimensional_inner_product_spaces

themathqueen committed 2 years ago

fbdbd949

moved files to new PR

themathqueen committed 2 years ago

a609fed1

feat(linear_algebra/invariant_submodule): invariant submodules

themathqueen committed 2 years ago

a7cd215b

refactor(topology): move `pcontinuous` etc to a new file (#18288)

urkud committed 2 years ago

2987594a

fix(*): add missing `classical` tactics and `decidable` arguments (#18277)

eric-wieser committed 2 years ago

6623e6af

feat(topology/algebra): add converse to tendsto.mul (#18276)

loefflerd committed 2 years ago

a81201cc

chore(test/gmonoid): Add a test of the gmonoid API (#18197)

eric-wieser committed 2 years ago

bbd198e1

feat(tactic/simps): store generated lemmas in attribute (#17964)

fpvandoorn committed 2 years ago

e3d9ab8f

chore(*): add mathlib4 synchronization comments (#18272)

leanprover-community-bot committed 2 years ago

63f84d91

feat(ring_theory/localization): localization of a basis, again (#18261)

Vierkantor committed 2 years ago

b69c9a77

fix after review

themathqueen committed 2 years ago

d984f884

doc(order/game_add): improve docstrings (#18269)

vihdzp committed 2 years ago

6f870fad

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

leanprover-community-bot committed 2 years ago

0be37584

refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade imports (#18217)

hrmacbeth committed 2 years ago

468b141b

feat(linear_algebra/dual): more about dual annihilator, some refactoring, and documentation (#17521)

kmill committed 2 years ago

68626536

feat(algebraic_geometry/elliptic_curve/weierstrass): define a basis for the coordinate ring (#18101)

Multramate committed 2 years ago

808ea4eb

themathqueen committed 2 years ago

2f5c69d0

refactor(data/nat/parity): reduce imports, add/delete lemmas (#18221)

urkud committed 2 years ago

8631e2d5

themathqueen committed 2 years ago

b6765404

chore(data/finsupp/defs): move lemmas out of the single section which are not about single (#18260)

eric-wieser committed 2 years ago

33694ffd

themathqueen committed 2 years ago

a0dc536a

Older