leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/normed_space/matrix_exponential): lemmas about the matrix exponential (#13520)

eric-wieser committed 3 years ago

bf8db9b7

rename(imo/imo1972_b2 → imo/imo1972_q5): Fix file name (#14037)

vihdzp committed 3 years ago

77c86ba4

feat(representation_theory/invariants): invariants of `lin_hom` are representation morphisms (#14012)

antoinelab01 committed 3 years ago

8412f1fc

feat(analysis/normed_space/exponential): Generalize `field` lemmas to `division_ring` (#13997)

eric-wieser committed 3 years ago

594ceda9

fix(tactics/alias): Make docstring calculation available to to_additive (#13968)

nomeata committed 3 years ago

afec1d73

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

a ton of progress

vihdzp committed 3 years ago

fbaf190e

vihdzp committed 3 years ago

34f7fafa

vihdzp committed 3 years ago

7438eb22

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

vihdzp committed 3 years ago

449ba97d

Remove classical

vihdzp committed 3 years ago

cfb64c17

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

Newer Older