leanprover-community/mathlib3

Pull Requests Commits

awainverse committed 4 years ago

a269bba5

awainverse committed 4 years ago

a5c86270

feat(geometry/manifold/mfderiv): differentiability of `f : E ≃L[𝕜] E'` (#6850)

urkud committed 4 years ago

f0bfb25c

feat(linear_algebra/dual): add the dual map (#6807)

kex-y committed 4 years ago

2b71c803

feat(topology/bcf): better dist_lt_of_* lemmas (#6781)

kim-em committed 4 years ago

8addf9a7

feat(ring_theory/polynomial/symmetric): degrees_esymm (#6718)

pechersky committed 4 years ago

6ae9f000

feat(group_theory/perm/sign): power has smaller support (#6872)

tb65536 committed 4 years ago

34a33172

feat(ring_theory/ideal/operations): add an instance (#6717)

riccardobrasca committed 4 years ago

adc5f9d6

chore(topology/sheaves): speed up a slow proof (#6879)

kim-em committed 4 years ago

fb495299

refactor(algebra/field): allow custom `div` (#6874)

urkud committed 4 years ago

c658f5cc

feat(group_theory/perm_basic): Lemma swap_apply_apply (#6870)

tb65536 committed 4 years ago

c07c3107

feat(measure_theory/interval_integral): weaken assumption in `integral_non_ae_measurable` (#6858)

benjamindavidson committed 4 years ago

0977b203

refactor(topology/algebra): define `has_continuous_smul`, use for topological semirings and algebras (#6823)

urkud committed 4 years ago

03f0bb1f

feat(category_theory/triangulated/rotate): add definition of rotation and inverse rotation of triangles and their morphisms (#6803)

l-kershaw committed 4 years ago

5c93c2d0

feat(topology/vector_bundle): definition of topological vector bundle (#4658)

Nicknamen committed 4 years ago

5c856c39

awainverse committed 4 years ago

4666bdcf

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

leanprover-community-bot committed 4 years ago

b797d519

feat(topology/bounded_continuous_function): add `coe_mul`, `mul_apply` (#6867)

ocfnash committed 4 years ago

e6d01b8e

chore(algebra/group/{pi,prod}): add missing instances (#6866)

eric-wieser committed 4 years ago

b6703916

feat(data/equiv/mul_add): define `mul_hom.inverse` (#6864)

ocfnash committed 4 years ago

6e14e8f9

refactor(topology/metric_space/antilipschitz): generalize to pseudo_metric_space (#6841)

riccardobrasca committed 4 years ago

e0547059

feat(algebra/geom_sum): rename geom_series to geom_sum, adds a lemma for the geometric sum (#6828)

paulvanwamelen committed 4 years ago

b299d144

chore(order/filter/lift,topology/algebra/ordered): drop `[nonempty ι]` (#6861)

urkud committed 5 years ago

1be91a1b

feat(logic/basic, logic/function/basic): make `cast` the simp-normal form of `eq.mp` and `eq.mpr`, add lemmas (#6834)

eric-wieser committed 5 years ago

879273e8

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

leanprover-community-bot committed 5 years ago

81e8a131

chore(measure_theory/measure): add `exists_measurable_superset_forall_eq` (#6853)

urkud committed 5 years ago

ec77f226

feat(data/equiv/basic): add a computable version of equiv.set.range (#6821)

eric-wieser committed 5 years ago

5a72dafd

feat(data/indicator_function): add multiplicative version (#6794)

urkud committed 5 years ago

c3034c27

feat(algebra/normed_space/basic,algebra/group_with_zero/power): real.(f)?pow_{even,bit0}_norm and field fpow lemmas (#6757)

pechersky committed 5 years ago

19e214e2

refactor(data/finsupp): add decidable_eq (#6333)

digama0 committed 5 years ago

039dfd2e

Newer Older