leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'imo2014q1' of https://github.com/leanprover-community/mathlib into imo2014q1

vihdzp committed 4 years ago

1ec95547

Merge branch 'master' into imo2014q1

vihdzp committed 4 years ago

2579649f

Update archive/imo/imo2014_q1.lean

vihdzp committed 4 years ago

Verified 773ce623

Update archive/imo/imo2014_q1.lean

vihdzp committed 4 years ago

Verified 466a1854

Update archive/imo/imo2014_q1.lean

vihdzp committed 4 years ago

Verified 2557d20a

Update archive/imo/imo2014_q1.lean

vihdzp committed 4 years ago

Verified ed278dcc

Update archive/imo/imo2014_q1.lean

vihdzp committed 4 years ago

Verified 5223c74b

Update archive/imo/imo2014_q1.lean

vihdzp committed 4 years ago

Verified 89f39e3a

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

Older