Commits leanprover-community/mathlib3

feat(topology/instances/nnreal): generalize `has_continuous_smul` instance (#16713)

j-loreaux committed 3 years ago

b2a65720

feat(data/fin): golf, add lemmas (#16711)

urkud committed 3 years ago

af90fef9

feat(group_theory/quotient_group): `simp` lemmas for `quotient_group.map` (#16703)

Vierkantor committed 3 years ago

d610cec7

feat(ring_theory/fractional_ideal): `simp` lemmas for `fractional_ideal.canonical_equiv` (#16702)

Vierkantor committed 3 years ago

001ba509

feat(algebra/hom/equiv): two little `simp` lemmas for `units.map_equiv` (#16701)

Vierkantor committed 3 years ago

acd02bbd

feat(topology/sheaves): presheaf on indiscrete space is sheaf iff value at empty is terminal (#16694)

alreadydone committed 3 years ago

3a0be826

feat(topology/continuous_function/{basic, compact}): add a few missing lemmas (#16714)

j-loreaux committed 3 years ago

9b1e9204

feat(analysis/normed_space/basic): add `norm_algebra_map_nnreal` (#16709)

j-loreaux committed 3 years ago

667f2a62

feat(data/fin): iff on add or sub across last-0 break (#15916)

pechersky committed 3 years ago

07e46bcf

feat(tactic/positivity): Extension for `finset.card` (#16637)

YaelDillies committed 3 years ago

4ed50443

feat(order/filter/{prod,pi}): add `filter.prod_le_prod`, `filter.pi_le_pi` etc (#16468)

urkud committed 3 years ago

6fc2df65

feat(order/filter/*): a family of pairwise disjoint filters has a family of pairwise disjoint members (#16504)

urkud committed 3 years ago

ed33fcf8

feat(topology/uniform_space/uniform_convergence_topology): bases for uniform structures of 𝔖-convergence (#14778)

ADedecker committed 3 years ago

71e28e0c

refactor(algebra/ring/basic): replace `neg_zero'` by `neg_zero_class` instance (#16686)

jsm28 committed 3 years ago

c8760bde

feat(data/set/intervals/monotone): extend a monotone function on a set to a globally monotone function (#16682)

sgouezel committed 3 years ago

d755c086

refactor(*): `inv_one_class`, `neg_zero_class` instances replacing lemmas (#16699)

jsm28 committed 3 years ago

42604284

feat(topology/algebra/algebra): `algebra_clm` does not need a normed space or field (#16690)

eric-wieser committed 3 years ago

2e09d790

feat(topology/path_connected): add five lemmas (#16501)

faenuccio committed 3 years ago

37cfab4b

feat(analysis/analytic/isolated_zeros): the uniqueness theorem for analytic fns (#16489)

vbeffara committed 3 years ago

a630444a

feat(number_theory/multiplicity): lifting the exponent lemma (#8915)

peakpoint committed 3 years ago

7944d185

chore(data/finset/lattice): use more common name, fix spaces (#16336)

astrainfinita committed 3 years ago

d95851bc

refactor(data/real/ennreal): `div_inv_one_monoid` instance (#16689)

jsm28 committed 3 years ago

78764375

refactor(data/real/ereal): `sub_neg_zero_monoid` instance (#16688)

jsm28 committed 3 years ago

0ec98ed0

refactor(algebra/periodic): use `neg_zero_class` for `antiperiodic.nat_mul_eq_of_eq_zero` (#16687)

jsm28 committed 3 years ago

8f89631e

feat(analysis/special_functions/pow): sqrt and inequalities (#16515)

mcdoll committed 3 years ago

e63a4d5e

feat(measure_theory/measure/lebesgue): deduce that a property is almost sure from a localized version in intervals (#16684)

sgouezel committed 3 years ago

345b38d6

feat(algebra/module/basic): weaken assumption (#16673)

astrainfinita committed 3 years ago

acc2a10b

feat(data/nat/parity): iterations of involutive functions (#16630)

urkud committed 3 years ago

0abedaf8

feat(tactic/push_neg): option for an alternate normal form of `¬ (P ∧ Q)` (#16586)

hrmacbeth committed 3 years ago

f7698588

chore(algebra/order/monoid_lemmas_zero_lt): reorder, create aliases (#16522)

astrainfinita committed 3 years ago

25e7fe6b