leanprover-community/mathlib

Pull Requests Commits

hrmacbeth committed 3 years ago

8ace4398

Apply suggestions from code review

dhruvbhatia00 committed 3 years ago

Verified fd933ec5

added docstring and added some tests

dhruvbhatia00 committed 3 years ago

5b3b136c

added a change suggested during code review

dhruvbhatia00 committed 3 years ago

2194ceca

Apply suggestions from code review

dhruvbhatia00 committed 3 years ago

Verified 6a7c4860

Update scripts/polyrith_sage.py

dhruvbhatia00 committed 3 years ago

Verified a33539b0

fixes for checks

dhruvbhatia00 committed 3 years ago

8b25defa

polyrith tactic created

dhruvbhatia00 committed 3 years ago

836d3259

fix(tactic/congrm): support multiple binders (#14753)

gebner committed 3 years ago

94fa33b4

chore(analysis/normed): move `normed.normed_field` to `normed.field.basic` (#14747)

urkud committed 3 years ago

430da94f

feat(data/finite/set): `finite` instances for set constructions (#14673)

kmill committed 3 years ago

6a0f9674

chore(a few random files): golfing using the new tactic `congrm` (#14593)

adomani committed 3 years ago

8eaeec26

refactor(algebra/group_with_zero/basic): Golf using division monoid lemmas (#14213)

YaelDillies committed 3 years ago

34ce7847

feat(dynamics/periodic_pts): `chain.pairwise` on orbit (#12991)

vihdzp committed 3 years ago

bbca2890

chore(analysis/normed/normed_field): golf 2 proofs (#14746)

urkud committed 3 years ago

46614736

chore(set_theory/ordinal/basic): golf ordinal addition definition (#14744)

vihdzp committed 3 years ago

dccdef6b

feat(analysis/normed_space): range of `norm` (#14740)

urkud committed 3 years ago

d2bfb32b

feat(analysis/convex): a convex set is contractible (#14732)

urkud committed 3 years ago

2aa3fd94

feat(data/complex/exponential): more `simp` lemmas (#14731)

urkud committed 3 years ago

7430d2d4

feat(data/fin/vec_notation): add has_reflect instance and tests (#14670)

eric-wieser committed 3 years ago

fee91d74

feat(probability/stopping): first hitting time (#14630)

kex-y committed 3 years ago

764d7a90

refactor(order/locally_finite): Allow `finset.Iix`/`finset.Ixi` on empty types (#14430)

YaelDillies committed 3 years ago

947c3c6d

feat(model_theory/semantics, elementary_maps): Defines elementary equivalence (#14723)

awainverse committed 3 years ago

114f5436

refactor(set_theory/game/*): fix theorem names (#14685)

vihdzp committed 3 years ago

9c40f30a

feat(model_theory/syntax, semantics): Mapping formulas given maps on terms and relations (#14466)

awainverse committed 3 years ago

c6677234

feat(tactic/ring): recursive ring_nf (#14429)

digama0 committed 3 years ago

ea976068

feat(linear_algebra/matrix): positive definite (#14531)

abentkamp committed 3 years ago

6e0e270d

docs(topology/basic): Fix typo in library note (#14743)

PatrickMassot committed 3 years ago

784c7034

golf(set_theory/game/pgame): golf `neg_le_neg_iff` (#14726)

alreadydone committed 3 years ago

1fbe1183

chore(analysis/convex/extreme): Make arguments semi-implicit (#14698)

YaelDillies committed 3 years ago

7958e7da

Older