leanprover-community/mathlib

Pull Requests Commits

chore(measure_theory/integral/bochner): use set_to_fun lemmas to prove integral properties (#10717)

RemyDegenne committed 3 years ago

2a8a01bc

feat(analysis/normed_space/spectrum): an algebra homomorphism into the base field is bounded (#11494)

dupuisf committed 3 years ago

905871f4

feat(measure_theory/measure): define `ae_disjoint` (#11500)

urkud committed 3 years ago

4e313969

feat(analysis/complex/cauchy_integral): review docs, add versions without `off_countable` (#11417)

urkud committed 3 years ago

50bdb297

doc(src/data/equiv/transfer_instances): nontrivial, not nonzero (#11508)

nomeata committed 3 years ago

391bd215

feat(data/finset/basic): `finset.two_lt_card` (#11505)

tb65536 committed 3 years ago

6b475a41

feat(analysis/special_functions/complex/arg): `arg_neg` lemmas (#11503)

jsm28 committed 3 years ago

079fb166

feat(order/well_founded_set): Antichains in a partial well order are finite (#11286)

YaelDillies committed 3 years ago

1c56a8de

feat(*): add a few lemmas about `function.extend` (#11498)

urkud committed 3 years ago

0d5bfd7b

feat(data/equiv/encodable): add a few lemmas (#11497)

urkud committed 3 years ago

9b70cc61

feat(algebra/star/unitary): lemmas about group_with_zero (#11493)

eric-wieser committed 3 years ago

ac76eb37

refactor(data/set/lattice): Generalize `mem_bUnion_iff` and `mem_bInter_iff` to dependent families (#11485)

vihdzp committed 3 years ago

a88ae0c4

feat(topology/metric_space): more lemmas about disjoint balls (#11506)

urkud committed 3 years ago

83eff323

feat(measure_theory): generalize some lemmas to `outer_measure` (#11501)

urkud committed 3 years ago

2f342b80

feat(measure_theory/measure): add lemmas, drop `measurable_set` assumptions (#11499)

urkud committed 3 years ago

43bbaee8

down to two sorries

dupuisf committed 3 years ago

757488ff

feat(*): add to_sub* lemmas for `map`, `fg` (#11480)

ericrbg committed 3 years ago

6d19ebaa

feat(analysis/special_functions/pow): tendsto rpow lemma for ennreals (#11475)

kex-y committed 3 years ago

4ed73168

chore(data/complex/basic): add of_real_eq_one (#11496)

eric-wieser committed 3 years ago

2c2338e7

feat(analysis/special_functions/complex/arg): `arg_conj`, `arg_inv` lemmas (#11479)

jsm28 committed 3 years ago

1f6bbf9e

feat(analysis/special_functions/trigonometric/angle): more 2π = 0 lemmas (#11482)

jsm28 committed 3 years ago

f4b93c8c

feat(number_field): notation for 𝓞 K, an algebra & ∈ 𝓞 K iff (#11476)

ericrbg committed 3 years ago

ed57bdd3

feat(order/filter/ultrafilter): add some comap_inf_principal lemmas (#11495)

berndlosert committed 3 years ago

5f5bcd85

feat(algebra/star/unitary): (re)define unitary elements of a star monoid (#11457)

dupuisf committed 3 years ago

d7f8f580

feat(analysis/calculus/dslope): define dslope (#11432)

urkud committed 3 years ago

1d1f3841

chore(*): Put `simp` attribute before `to_additive` (#11488)

YaelDillies committed 3 years ago

1aee8a8d

refactor(analysis/normed_space): merge `normed_space` and `semi_normed_space` (#8218)

eric-wieser committed 3 years ago

02a4775a

feat(analysis/seminorm): Add `has_add` and `has_scalar nnreal` (#11414)

mcdoll committed 3 years ago

d60541cc

feat(algebra/star/basic): change `star_ring_aut` (notably, complex conjugation) from `ring_equiv` to `ring_hom` and make type argument explicit (#11418)

hrmacbeth committed 3 years ago

3fb5b82e

dupuisf committed 3 years ago

5a61431e

Newer Older