leanprover-community/mathlib3

Pull Requests Commits
Merge remote-tracking branch 'origin/master' into group_ring_lemmas
kim-em committed 5 years ago
631e74e4
chore(scripts/deploy_docs.sh): skip gen_docs if already built (#2263)
bryangingechen committed 5 years ago
Verified 1b13ccdf
chore(data/int/basic): change instance order (#2257)
sgouezel committed 5 years ago
Verified 211c5d11
slight improvement
kim-em committed 5 years ago
9b74291b
sadness
kim-em committed 5 years ago
3187927c
chore(scripts): update nolints.txt
leanprover-community-bot committed 5 years ago
3c0b35c4
feat(algebra/ring): generalize mul_ite (#2223)
kim-em committed 5 years ago
Verified d0a85073
Merge branch 'mul_ite' into group_ring_lemmas
kim-em committed 5 years ago
347c54cb
Merge branch 'master' into mul_ite
mergify[bot] committed 5 years ago
Verified 3ebb7326
feat(logic/basic): trivial transport lemmas (#2254)
kim-em committed 5 years ago
Verified 786c7375
chore(tactic/lint): typo (#2253)
kim-em committed 5 years ago
Verified 451de279
chore(tactic/*): update tags (#2224)
robertylewis committed 5 years ago
Verified 21ad1d3a
chore(ci): update nolints before docs and leanchecker (#2250)
robertylewis committed 5 years ago
Verified d3cbd4d0
remove simp from add_ite, add comment
kim-em committed 5 years ago
b5ab0024
gross fix for quadratic reciprocity argument
kim-em committed 5 years ago
ba3883a6
cast_ite
kim-em committed 5 years ago
5b39eccc
fix prod_ite as well
kim-em committed 5 years ago
2c31f6f5
handing it back to CI for another try
kim-em committed 5 years ago
b8c7f28d
fix
kim-em committed 5 years ago
8d08725b
chore(.mergify.yml): cleanup (#2248)
bryangingechen committed 5 years ago
Verified de39b9a8
doc(docs/install/project.md): mention that projects are git repositories (#2244)
bryangingechen committed 5 years ago
Verified 2fbf0070
feat(data/equiv/local_equiv): construct from `bij_on` or `inj_on` (#2232)
urkud committed 5 years ago
Verified 75b4ee86
feat(topology/algebra/module): define `fst` and `snd`, review (#2247)
urkud committed 5 years ago
Verified 8943351e
chore(scripts): update nolints.txt
leanprover-community-bot committed 5 years ago
5b443634
refactor(data/set/function): move `function.restrict` to `set`, redefine (#2243)
urkud committed 5 years ago
Verified 0fc4e6a8
trying again, with better definitional module structure
kim-em committed 5 years ago
84799258
err.. marking simp again, because I can't remember what goes wrong and need CI to compile for me
kim-em committed 5 years ago
fb3ae405
working
kim-em committed 5 years ago
61a98243
chore(scripts): update nolints.txt
leanprover-community-bot committed 5 years ago
fa36a8ef
feat(data/equiv/functor): bifunctor.map_equiv (#2241)
kim-em committed 5 years ago
Verified ea10e173
Terms Of Use Privacy Policy Refund Policy Impressum