leanprover-community/mathlib

Pull Requests Commits

chore(algebra/regular/*): generalisation linter (#13955)

ericrbg committed 3 years ago

34b61e3d

feat(algebra/category/Module/basic): `iso.hom_congr`agrees with `linear_equiv.arrow_congr` (#13954)

antoinelab01 committed 3 years ago

52531532

feat(set_theory/pgame/birthday): Birthdays of ordinals (#13714)

vihdzp committed 3 years ago

4f386e66

feat(algebraic_topology/dold_kan): defining some null homotopic maps (#13085)

joelriou committed 3 years ago

1e8f3817

refactor(algebra/{group,group_with_zero/basic): Generalize lemmas to division monoids (#14000)

YaelDillies committed 3 years ago

bf6e13bf

refactor(data/nat/log): Golf + improved theorem names (#14019)

vihdzp committed 3 years ago

449ba97d

feat(topology/algebra/infinite_sum): add `tsum_star` (#13999)

eric-wieser committed 3 years ago

163ef61e

fix(topology/algebra/module/weak_dual): fix namespace issue, add a few extra lemmas (#13407)

dupuisf committed 3 years ago

dd16a836

feat(linear_algebra/linear_pmap): `mk_span_singleton` of the same point (#14029)

YaelDillies committed 3 years ago

69c07a4b

feat(measure_theory/integral): a few more integral lemmas (#14025)

sgouezel committed 3 years ago

6a5d17ee

feat(analysis/p_series): explicit bounds on sums of the form 1/j^2 (#13851)

sgouezel committed 3 years ago

e3306942

chore(algebra/category/CommRing=>Ring): rename (#14022)

kim-em committed 3 years ago

79ffb556

feat(probability/ident_distrib): identically distributed random variables (#14024)

sgouezel committed 3 years ago

3478a2af

feat(algebra/category/Module): biproducts (#13908)

kim-em committed 3 years ago

0c64b3d3

feat(set_theory/ordinal/basic): Supremum indexed over an empty / unique type (#13735)

vihdzp committed 3 years ago

ce0dc836

chore(logic/relation): Dot notation on `well_founded.trans_gen` (#14016)

vihdzp committed 3 years ago

3a0eb4b5

feat(data/rat/meta_defs, meta/expr): rat.to_pexpr and int.to_pexpr (#14002)

robertylewis committed 3 years ago

e1902256

feat(algebra/{invertible + group_power/lemmas}): taking `inv_of` (⅟_) is injective (#14011)

adomani committed 3 years ago

e0dd3003

chore(order/*): Less `order_dual` abuse (#14008)

YaelDillies committed 3 years ago

0e494afe

chore(order/filter/pointwise): Better definitional unfolding (#13941)

YaelDillies committed 3 years ago

51667657

feat(probability/variance): define the variance of a random variable, prove its basic properties (#13912)

sgouezel committed 3 years ago

cf65daf0

feat(group_theory/group_action/units): simp lemma for scalar action of `is_unit.unit h` (#14006)

sgouezel committed 3 years ago

c2476223

feat(combinatorics/simple_graph/hasse): Hasse diagram and path graph (#13959)

YaelDillies committed 3 years ago

9134a8e7

feat(analysis/calculus/deriv): generalize some lemmas (#13575)

astrainfinita committed 3 years ago

b2aa27e3

feat(algebra/module/linear_map): `Rᵐᵒᵖ` is isomorphic to `module.End R R` (#13931)

haruhisa-enomoto committed 3 years ago

f8bc097d

feat(order/filter): add a few lemmas (#13985)

urkud committed 3 years ago

559f58b1

refactor(algebra/order/monoid_lemmas): reorder the file (#13492)

astrainfinita committed 3 years ago

ca1375a5

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

leanprover-community-bot committed 3 years ago

5789c637

feat(order/atoms): is_atomic_of_order_bot_lt_well_founded (#13967)

kim-em committed 3 years ago

275dabfc

feat(analysis/locally_convex/with_seminorms): characterization of the topology induced by seminorms in terms of `𝓝 0` (#13547)

ADedecker committed 3 years ago

dcd452de

Newer Older