leanprover-community/mathlib

Pull Requests Commits
feat(tactic/conv/apply_congr): using congruence lemmas inside conv (#2221)
kim-em committed 6 years ago
Verified efdc8504
feat(tactic/show_term): show_term { t } prints the term constructed by t (#2227)
kim-em committed 6 years ago
Verified 5437b10a
feat(data/equiv): sigma_congr (#2205)
kim-em committed 6 years ago
Verified 5f376b26
chore(README,docs/*): replace tactic doc files with links to mathlib docs (#2225)
bryangingechen committed 6 years ago
Verified bb6e1d4f
feat(linear_algebra): add range_le_ker_iff (#2229)
TwoFX committed 6 years ago
Verified b5044302
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
6a7e55e4
doc(data/int/gcd): attribution + module doc (#2217)
bryangingechen committed 6 years ago
Verified 9a9794d7
refactor(topology/metric_space/contracting): redefine using emetric (#2070)
urkud committed 6 years ago
Verified 9832fba5
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
25df50e6
feat(analysis/convex.cone): prove M. Riesz extension theorem, Hahn-Banach theorem (#2120)
urkud committed 6 years ago
Verified 5b2c9521
chore(ring_theory/algebra): generalize restrict_scalars to noncommutative algebras (#2216)
kim-em committed 6 years ago
Verified d3d78a98
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
fe40a15a
feat(algebra/module): `f : E →+ F` is `ℚ`-linear (#2215)
urkud committed 6 years ago
Verified 6aa5572e
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
b9ee94d8
fix(tactic/transport): make `to_additive` copy `protected`status (#2212)
urkud committed 6 years ago
Verified 7f103fd3
feat(tactic/doc_commands): allow doc strings on add_tactic_doc (#2201)
gebner committed 6 years ago
Verified 6febc8c0
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
4e46b306
chore(linear_algebra/*): rename copair, pair to coprod, prod (#2213)
bryangingechen committed 6 years ago
Verified 7d02c231
feat(ring_theory/algebra) : generalize `rat.algebra_rat` to `division_ring` (#2208)
urkud committed 6 years ago
Verified 3a714995
fix(linear_algebra/basic): make R explicit in linear_equiv.refl (#2161)
kbuzzard committed 6 years ago
Verified 9485a857
doc(ring_theory/adjoin_root): add docstring (#2211)
kbuzzard committed 6 years ago
Verified 19de4162
merge
kim-em committed 6 years ago
fcdaf6f3
merge
kim-em committed 6 years ago
ef99e91a
revert accidental push to master
kim-em committed 6 years ago
09401b7f
feat(tactic/core): trace_for
kim-em committed 6 years ago
3375126c
blech
kim-em committed 6 years ago
5b3a3c0e
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
af0cf30e
refactor(scripts/mk_nolint): produce nolints.txt file during linting (#2194)
gebner committed 6 years ago
Verified 0bd8b94d
doc(docs/contribute/index.md): remove obsolete recommendation to use lean-3.7.2 branch (#2206)
gebner committed 6 years ago
Verified dd85db0c
chore(leanpkg.toml): Lean 3.7.2c (#2203)
bryangingechen committed 6 years ago
Verified bc84a205
Terms Of Use Privacy Policy Refund Policy Impressum