Commits leanprover-community/mathlib

feat(topology/continuous_function/bounded): register instances of `star` structures (#10570)

j-loreaux committed 4 years ago

e618cfe3

fix(tactic/ring): instantiate metavariables (#10589)

digama0 committed 4 years ago

25386262

feat(algebra/algebra/spectrum): lemmas when scalars are a field (#10476)

j-loreaux committed 4 years ago

94783bef

feat(data/finsupp/basic): lemmas on the support of the `tsub` of `finsupp`s (#10651)

stuart-presnell committed 4 years ago

08215b55

feat(measure_theory/integral/set_to_l1): properties of (dominated_)fin_meas_additive (#10590)

RemyDegenne committed 4 years ago

9ef122d2

feat(group_theory/submonoid): The monoid_hom from a submonoid to its image. (#10680)

erdOne committed 4 years ago

c23b54c7

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

urkud committed 4 years ago

97e44687

feat(order/filter,topology/instances/real): lemmas about `at_top`, `at_bot`, and `cocompact` (#10652)

urkud committed 4 years ago

bfe595d3

chore(measure_theory/function/conditional_expectation): change condexp notation (#10584)

RemyDegenne committed 4 years ago

e3d9adf1

feat(topology/instances/real_vector_space): add an `is_scalar_tower` instance (#10490)

urkud committed 4 years ago

70171ac4

chore(algebra/direct_limit): remove module.directed_system (#10636)

eric-wieser committed 4 years ago

4efa9d8a

feat(analysis/normed_space/weak_dual): add polar sets in preparation for Banach-Alaoglu theorem (#9836)

kkytola committed 4 years ago

11bf7e52

doc(data/nat/prime): fix links (#10677)

ericrbg committed 4 years ago

fc3116f9

feat(data/finset/basic): val_le_iff_val_subset (#10603)

isadofschi committed 4 years ago

ab316732

feat(data/mv_polynomial/basic) induction_on'' (#10621)

isadofschi committed 4 years ago

60c1d60e

feat(data/int/basic): add `nat_abs_eq_nat_abs_iff_*` lemmas for nonnegative and nonpositive arguments (#10611)

stuart-presnell committed 4 years ago

e14dc11a

refactor(data/matrix): reverse the direction of `matrix.minor_mul_equiv` (#10657)

Vierkantor committed 4 years ago

baab5d30

feat(data/list/range): fin_range_succ_eq_map (#10654)

eric-wieser committed 4 years ago

2ea1fb68

chore(algebra/tropical/basic): golf and clean (#10633)

pechersky committed 4 years ago

fdb773a2

refactor(data/complex/is_R_or_C): `finite_dimensional.proper_is_R_or_C` is not an `instance` anymore (#10629)

urkud committed 4 years ago

bcd9a745

feat(algebra/graded_monoid): add lemmas about power and product membership (#10627)

eric-wieser committed 4 years ago

e289343a

fix(data/finsupp/basic): add missing decidable arguments (#10672)

eric-wieser committed 4 years ago

1d0bb865

refactor(data/finsupp): use `{f : α →₀ M | ∃ a b, f = single a b}` instead of union of ranges (#10671)

urkud committed 4 years ago

2ce95ca8

feat(measure_theory/probability_mass_function): Calculate supports of pmf constructions (#10371)

dtumad committed 4 years ago

8ab1b3b4

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