leanprover-community/mathlib

Pull Requests Commits
feat(data/complex/basic): of_real_fpow (#640)
ChrisHughes24 committed 6 years ago
fc529b6f
docs(tactic/monotonicity/interactive): fix `mono` documentation [ci-skip]
rwbarton committed 6 years ago
d7d90fa6
fix build
rwbarton committed 6 years ago
0924ac0e
refactor(*): use decidable_linear_order.lift
rwbarton committed 6 years ago
a0e2de96
feat(data/equiv/algebra): ring equiv for mv_polynomial
kckennylau committed 6 years ago
7cfcce3d
feat(tactic/interactive.lean): clear_aux_decl
ChrisHughes24 committed 6 years ago
54f4b291
feat(field_theory/splitting_field): splits predicate on polynomials
ChrisHughes24 committed 6 years ago
8faf8df0
move continuous_of_lipschitz around
sgouezel committed 6 years ago
8ee4f2da
feat(measure_theory): integral is equal and monotone almost-everywhere and for measurable functions it is a.e. strict at 0
johoelzl committed 6 years ago
83edba46
Move tendsto_div to a better place
sgouezel committed 6 years ago
cd41acab
refactor(category_theory/opposites): Make `opposite` irreducible
rwbarton committed 6 years ago
042c290d
feat(category_theory/limits/cones): forgetful functors
rwbarton committed 6 years ago
d1b7d914
feat(*) refactor module
kckennylau committed 6 years ago
b39d6d8a
fix(topology/instances/ennreal): fix merge
johoelzl committed 6 years ago
fd3e5a12
add ennreal.to_real
sgouezel committed 6 years ago
e62c534c
feat(topology): prove continuity of nndist and edist; `ball a r` is a metric space
johoelzl committed 6 years ago
8572c6b0
refactor(linear_algebra/direct_sum_module): move to algebra/direct_sum
kckennylau committed 6 years ago
afa31bed
chore(linear_algebra/dimension): simplify dim_add_le_dim_add_dim
johoelzl committed 6 years ago
7199bb36
feat(ring_theory/algebra): remove out_param
kckennylau committed 6 years ago
038e0b27
feat(ring_theory/algebra): remove of_core
kckennylau committed 6 years ago
af7a7ee3
feat(ring_theory/algebra): make algebra a class
kckennylau committed 6 years ago
79ba61cc
feat(ring_theory/algebra): define algebra over a commutative ring
kckennylau committed 6 years ago
a0b6cae4
feat(category_theory/isomorphism): as_iso
rwbarton committed 6 years ago
1d2eda7b
feat(category_theory/types): conversions between iso and equiv
rwbarton committed 6 years ago
ccd895f8
refactor(category_theory/concrete_category): move `bundled` to own file
rwbarton committed 6 years ago
d074b51b
feat(category_theory/full_subcategory): induced categories
rwbarton committed 6 years ago
50398e50
feat(analysis/exponential): complex powers
ChrisHughes24 committed 6 years ago
19c2f68c
feat(data/complex/exponential): exp_eq_one_iff
ChrisHughes24 committed 6 years ago
c0577580
refactor(algebra/field_power): notation for fpow
ChrisHughes24 committed 6 years ago
db691737
feat(order/conditionally_complete_lattice): cinfi_const (#634)
sgouezel committed 6 years ago
d359aa89
Terms Of Use Privacy Policy Refund Policy Impressum