Commits leanprover-community/mathlib

feat(topology/algebra/group): Addition of interiors (#10659)

YaelDillies committed 4 years ago

678566f2

feat(measure_theory/integral): `∫ x in b..b+a, f x = ∫ x in c..c + a, f x` for a periodic `f` (#10477)

urkud committed 4 years ago

eedb906c

fix(data/finsupp/basic): add missing decidable argument (#10649)

eric-wieser committed 4 years ago

4d56716d

fix(algebra/direct_sum): change `ring_hom_ext` to not duplicate `ring_hom_ext'` (#10640)

eric-wieser committed 4 years ago

e5ba338e

feat(category_theory): Filtered colimits preserves finite limits in algebraic categories (#10604)

erdOne committed 4 years ago

b495fdfd

feat(analysis/normed_space/operator_norm): module and norm instances on continuous semilinear maps (#10494)

dupuisf committed 4 years ago

2bfa7684

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

leanprover-community-bot committed 4 years ago

1a92bc97

chore(measure_theory/integral/set_to_l1): change definition of dominated_fin_meas_additive (#10585)

RemyDegenne committed 4 years ago

eaa9e876

feat(topology/algebra/ordered/basic): Interior of `{x | f x ≤ g x}` (#10653)

YaelDillies committed 4 years ago

54aeec74

feat(measure_theory/lattice): define typeclasses for measurability of lattice operations, define a lattice on ae_eq_fun (#10591)

RemyDegenne committed 4 years ago

a803e21d

feat(field_theory/finite/basic): generalize lemma from field to integral domain (#10655)

ChrisHughes24 committed 4 years ago

ae7a88d1

feat(data/pi): add `pi.single_inj` (#10644)

eric-wieser committed 4 years ago

9a2c2998

feat(algebra/category): (co)limits in CommRing (#10593)

erdOne committed 4 years ago

03dd404a

feat(topology/sheaves): `F(U ⨿ V) = F(U) × F(V)` (#10597)

erdOne committed 4 years ago

173a21ab

feat(topology/algebra/ordered/basic): Add alternative formulations of four lemmas. (#10630)

kkytola committed 4 years ago

ba1cbfac

chore(*): fix last line length and notation style linter errors (#10642)

robertylewis committed 4 years ago

90319890

feat(data/int/basic): four lemmas about integer divisibility (#10602)

stuart-presnell committed 4 years ago

cd857f77

feat(algebra/geom_sum): criteria for 0 < geom_sum (#10567)

ericrbg committed 4 years ago

eec4b70c

feat(linear_algebra/determinant): linear_equiv.det_mul_det_symm (#10635)

jsm28 committed 4 years ago

a8c086fe

feat(data/multiset): add some lemmas about filter (eq x) (#10626)

Ruben-VandeVelde committed 4 years ago

1d5202ae

feat(linear_algebra/multilinear/basic,linear_algebra/alternating): comp_linear_map lemmas (#10631)

jsm28 committed 4 years ago

81243140

chore(linear_algebra/affine_space/basis): remove unhelpful coercion (#10637)

ocfnash committed 4 years ago

f50984d8

chore(analysis/inner_product/projections): generalize some lemmas (#10608)

urkud committed 4 years ago

e6ad0f29

refactor(order/atoms): is_simple_order from is_simple_lattice (#10537)

pechersky committed 4 years ago

e726945e

chore(scripts/mk_all.sh): allow 'mk_all.sh ../test' (#10628)

kim-em committed 4 years ago

e7bd49f2

chore(combinatorics/simple_graph/coloring): remove extra asterisk (#10618)

kmill committed 4 years ago

2b2d1167

feat(ring_theory/graded_algebra): projection map of graded algebra (#10116)

jjaassoonn committed 4 years ago

8c1f2b5d

feat(topology/continuous_function/bounded): continuous bounded real-valued functions form a normed vector lattice (#10322)

mans0954 committed 4 years ago

428b9e55

chore(data/stream): merge `basic` into `init` (#10617)

urkud committed 4 years ago

37f343cf

fix(topology/algebra/uniform_field): remove unnecessary topological_r… (#10614)

kbuzzard committed 4 years ago

6eeb54e6