leanprover-community/mathlib3

Pull Requests Commits

feat(probability/martingale): add some lemmas for submartingales (#14904)

kex-y committed 3 years ago

f94a64f7

feat(topology/metric_space): a countably generated uniformity is metrizable (#14052)

urkud committed 3 years ago

40fa2d84

refactor(algebra/order/monoid): use typeclasses instead of lemmas (#14848)

urkud committed 3 years ago

fe322e12

feat(linear_algebra/{multilinear, alternating}): add `cod_restrict` and lemmas (#14927)

eric-wieser committed 3 years ago

0e5f278d

feat(data/finite/basic): add missing instances (#14913)

urkud committed 3 years ago

3e326fcb

chore(topology/basic): golf a proof (#14911)

urkud committed 3 years ago

363bbd22

refactor(data/polynomial): extract/add lemmas and golf (#14888)

alreadydone committed 3 years ago

475cf379

feat(probability/independence): equivalent ways to check indep_fun (#14814)

RemyDegenne committed 3 years ago

dabb0c61

feat(field_theory.intermediate_field): intermediate_field.inclusion (#12596)

Sebastian-Monnet committed 3 years ago

7c2ad75e

feat(data/int/basic): add a better `has_reflect int` instance (#14906)

eric-wieser committed 3 years ago

e420232b

feat(meta/univs): Add a reflect_name tactic, make reflected instances universe polymorphic (#14766)

eric-wieser committed 3 years ago

f05c49f6

feat(data/finset/pointwise): `s • t` is the union of the `a • t` (#14696)

YaelDillies committed 3 years ago

8187142b

feat(ring_theory/trace): Add `trace_eq_sum_automorphisms`, `norm_eq_prod_automorphisms`, `normal.alg_hom_equiv_aut` (#14523)

isadofschi committed 3 years ago

6d00cc21

chore(order/filter): turn `tendsto_id'` into an `iff` lemma (#14791)

urkud committed 3 years ago

efe794c3

feat(measure_theory/function/conditional_expectation): conditional expectation w.r.t. the restriction of a measure to a set (#14751)

RemyDegenne committed 3 years ago

6cefaf4b

feat(data/real/{e,}nnreal): add some order isomorphisms (#14900)

urkud committed 3 years ago

ac2e9dbf

refactor(order/complete_lattice): `Sup` lemmas before `Inf` lemmas (#14868)

vihdzp committed 3 years ago

cb948930

chore(*): Disparate generalizations to division monoids (#14686)

YaelDillies committed 3 years ago

649ca66b

feat(data/finset): add some lemmas about `finset.disj_union` (#14910)

eric-wieser committed 3 years ago

56185bdd

refactor(ring_theory): generalize basic API of `ring_hom` to `ring_hom_class` (#14756)

dupuisf committed 3 years ago

198cb64d

chore(data/nat,int): move field-specific lemmas about cast (#14890)

Vierkantor committed 3 years ago

44d3fc00

feat(data/set): replace `set_coe.can_lift` by `subtype.can_lift` (#14792)

urkud committed 3 years ago

c3e3d1aa

feat(analysis/../log): log_nat_eq_sum_factorization (#14782)

ericrbg committed 3 years ago

4de20c56

feat(data/polynomial/erase_lead): Characterizations of polynomials of small support (#14500)

tb65536 committed 3 years ago

c2fcf9f1

feat(order/hom/basic): some lemmas about order homs and equivs (#14872)

Paul-Lez committed 3 years ago

ef24aced

feat(analysis/convex/strict_convex_space): isometries of strictly convex spaces are affine (#14837)

jsm28 committed 3 years ago

dd2e7add

feat(group_theory/finite_abelian): Structure of finite abelian groups (#14736)

pbazin committed 3 years ago

966bb245

feat(analysis/seminorm): add add_group_seminorm (#14336)

mariainesdff committed 3 years ago

cff439d8

feat(number_theory): define ramification index and inertia degree (#14332)

Vierkantor committed 3 years ago

585a1bf3

feat(data/sigma,data/ulift,logic/equiv): add missing lemmas (#14903)

urkud committed 3 years ago

cc4b8e55

Newer Older