leanprover-community/mathlib3

Pull Requests Commits

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

Nicknamen committed 5 years ago

5c856c39

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

leanprover-community-bot committed 5 years ago

b797d519

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

ocfnash committed 5 years ago

e6d01b8e

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

eric-wieser committed 5 years ago

b6703916

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

ocfnash committed 5 years ago

6e14e8f9

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

riccardobrasca committed 5 years ago

e0547059

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

paulvanwamelen committed 5 years ago

b299d144

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

urkud committed 5 years ago

1be91a1b

sgouezel committed 5 years ago

ea9b9151

sgouezel committed 5 years ago

a0c9fe63

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

benjamindavidson committed 5 years ago

6ece8b85

chore(data/zmod/basic): make `fin.comm_ring.sub` defeq to `fin.sub` (#6848)

eric-wieser committed 5 years ago

77c3bfed

feat(algebra/big_operators/ring): add finset.prod_[one_]sub_ordered (#6811)

urkud committed 5 years ago

ab2c44c4

feat(tactic/lint): linter for @[class] def (#6061)

digama0 committed 5 years ago

b4373e5a

more dot notation

sgouezel committed 5 years ago

08442ce0

ae_measurable_comp_right_iff_of_closed_embedding

sgouezel committed 5 years ago

4ae5e4c0

chore(algebra/algebra/subalgebra): Add missing coe_sort for subalgebra (#6800)

eric-wieser committed 5 years ago

a7563333

chore(*): removing some completed TODOs (#6844)

kim-em committed 5 years ago

144e9c4b

chore(category_theory/triangulated): cleanup (#6827)

kim-em committed 5 years ago

67730166

feat(algebra/category): subobjects in the category of R-modules (#6842)

TwoFX committed 5 years ago

beb2cc98

chore(data/nat/basic): add @[simp] to some lemmas about numerals (#6652)

kim-em committed 5 years ago

935003eb

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

leanprover-community-bot committed 5 years ago

e0a79186

feat(logic/basic): `is_trans Prop iff` instance (#6836)

gebner committed 5 years ago

94a4a958

Newer Older