Commits leanprover-community/mathlib

feat(topology/metric_space/lipschitz): add several lemmas (#15634)

urkud committed 3 years ago

d43aef06

feat(order/filter/*): `filter.pi` is countably generated (#15632)

urkud committed 3 years ago

a095eaeb

chore(algebra/jordan/basic): remove unused imports (#15686)

eric-wieser committed 3 years ago

4b76b9d6

refactor(category_theory/*): use simps in the old parts of the library (#14236)

kim-em committed 3 years ago

59382264

feat(algebra/jordan): Introduce Jordan rings (#11073)

mans0954 committed 3 years ago

edb7f923

doc(tactic/compute_degree): fix tactic tags, add examples to docs (#15680)

robertylewis committed 3 years ago

9d8c0f82

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

leanprover-community-bot committed 3 years ago

df09f2a7

feat(big_operators/fin): sum over elements of vector equal to `a` equals count `a` (#15360)

dtumad committed 3 years ago

1142e0b7

chore(tactic/fix_reflect_string): delete file (#15537)

hrmacbeth committed 3 years ago

d85af62f

feat(data/set/countable): add `iff` versions of some lemmas (#15671)

urkud committed 3 years ago

8da80f4e

feat(measure_theory/measure/finite_measure_weak_convergence): Add normalization of finite measures to probability measures and characterize weak convergence in terms of it. (#15528)

kkytola committed 3 years ago

f22fe49a

feat(algebra/lie/of_associative): add `commute.lie_eq` (#15675)

eric-wieser committed 3 years ago

fe45ef24

feat(data/sign): `left.sign_neg`, `right.sign_neg` (#15652)

jsm28 committed 3 years ago

c7ae1acf

refactor(measure_theory/function/uniform_integrable): change `uniform_integrable` to only require `ae_strongly_measurable` (#15623)

kex-y committed 3 years ago

287a69a0

feat(combinatorics/set_family/kleitman): Kleitman's bound (#14543)

YaelDillies committed 3 years ago

a6269fe6

feat(order/compare): general cleanup (#15665)

vihdzp committed 3 years ago

b877056e

feat(linear_algebra/annihilating_polynomial): add definition of annihilating ideal and show minpoly generates in field case (#12140)

twoquarterrican committed 3 years ago

98f0d695

feat(data/matrix/basic): Add `alg_equiv` and `linear_equiv` instances for transpose. (#15386)

linesthatinterlace committed 3 years ago

d244509f

feat(*/partition_of_unity): more lemmas based on the partition of unity (#15609)

urkud committed 3 years ago

168d6ba8

feat(category_theory/preadditive/*): algebra over endofunctor preadditive and forget additive functor (#15100)

Julian-Kuelshammer committed 3 years ago

f5138d15

fix(algebraic_geometry/projective_spectrum/scheme) : fix module doc string (#15633)

jjaassoonn committed 3 years ago

62a1f82f

feat(algebraic_geometry/morphisms): Basic framework for classes of morphisms between schemes (#14944)

erdOne committed 3 years ago

b351ad53

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

leanprover-community-bot committed 3 years ago

44c1fdca

chore(algebra/module/basic): use `simp` instead of `norm_num` (#15670)

urkud committed 3 years ago

48dec300

chore(algebra/order/sub): Generalize lemmas (#15497)

YaelDillies committed 3 years ago

5f543bd9

feat(analysis/normed_space/lp_space): construct star structures on lp spaces (#15317)

JonBannon committed 3 years ago

3419dfc0

refactor(set_theory/ordinal/basic): `ordinal.min` → `infi` (#14707)

vihdzp committed 3 years ago

a1ce53c0

feat(representation_theory/Rep): Rep k G ≌ Module (monoid_algebra k G) (#13713)

kim-em committed 3 years ago

5ed2c728

feat(algebra/periodic): `fract_periodic` (#15660)

jsm28 committed 3 years ago

86febe13

feat(order/bounded_order): an order is either an `order_bot` or a `no_bot_order` (#15636)

vihdzp committed 3 years ago

75f10446