Commits leanprover-community/mathlib3

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

YaelDillies committed 4 years ago

69c07a4b

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

sgouezel committed 4 years ago

6a5d17ee

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

sgouezel committed 4 years ago

e3306942

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

kim-em committed 4 years ago

79ffb556

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

sgouezel committed 4 years ago

3478a2af

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

kim-em committed 4 years ago

0c64b3d3

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

vihdzp committed 4 years ago

ce0dc836

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

vihdzp committed 4 years ago

3a0eb4b5

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

robertylewis committed 4 years ago

e1902256

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

adomani committed 4 years ago

e0dd3003

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

YaelDillies committed 4 years ago

0e494afe

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

YaelDillies committed 4 years ago

51667657

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

sgouezel committed 4 years ago

cf65daf0

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

sgouezel committed 4 years ago

c2476223

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

YaelDillies committed 4 years ago

9134a8e7

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

astrainfinita committed 4 years ago

b2aa27e3

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

haruhisa-enomoto committed 4 years ago

f8bc097d

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

urkud committed 4 years ago

559f58b1

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

astrainfinita committed 4 years ago

ca1375a5

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

leanprover-community-bot committed 4 years ago

5789c637

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

kim-em committed 4 years ago

275dabfc

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

ADedecker committed 4 years ago

dcd452de

feat(topology/algebra/module/basic): basic topological properties of quotient modules (#13433)

ADedecker committed 4 years ago

10721bab

feat(ring_theory/localization): generalize lemmas from `comm_ring` to `comm_semiring` (#13994)

yuma-mizuno committed 4 years ago

8f116f43

chore(analysis/normed_space/exponential): Make the `𝔸` argument implicit (#13986)

eric-wieser committed 4 years ago

27e105d2

feat(number_theory/legendre_symbol/*): add results on value at -1 (#13978)

MichaelStollBayreuth committed 4 years ago

eea16dc8

feat(data/polynomial/laurent): laurent polynomials -- defs and some API (#13784)

adomani committed 4 years ago

dfe1897f

feat(tactic/lint/misc): adding a linter that flags iffs with explicit variables on both sides (#11606)

arthurpaulino committed 4 years ago

58d83ed5

docs(ring_theory/localization/ideal): fix an unused name (#13992)

yuma-mizuno committed 4 years ago

863a1676

chore(data/zmod/basic.lean): change order of arguments of `zmod.nat_cast_mod` for consistency (#13988)

MichaelStollBayreuth committed 4 years ago

db5c2a6d