Commits leanprover-community/mathlib3

feat(probability/integration): remove integrability assumption in indep_fun.integral_mul (#16167)

sgouezel committed 3 years ago

de62604b

chore(category_theory): fix name of mono_app_of_mono (#16275)

joelriou committed 3 years ago

937c692d

fix(combinatorics/composition): remove non-terminal simp (#16259)

gebner committed 3 years ago

8dd80093

feat(algebra/order/field): Canonically linear ordered semifields (#15677)

YaelDillies committed 3 years ago

1c2d71f1

feat(data/rat/defs): add two lemmas for `pnat_denom` of 0 and 1 (#15864)

joneugster committed 3 years ago

ebb53dc3

chore(category_theory/limits/shapes/finite_products): avoid tidy (#16261)

gebner committed 3 years ago

6901db60

docs(ring_theory/valuation/valuation_subring): clarify value group docstring (#16272)

kbuzzard committed 3 years ago

c241a033

feat(category_theory): coseparators in structured_arrow (#15981)

TwoFX committed 3 years ago

fef8efdf

feat(measure_theory/measure/finite_measure_weak_convergence): Add portmanteau implications concerning open and closed sets. (#15321)

kkytola committed 3 years ago

c95908a6

feat(ring_theory/ideal): Two little `restrict_scalars` lemmas (#16248)

Vierkantor committed 3 years ago

18361694

feat(analysis/normed_space/star/spectrum): star algebra morphisms over ℂ are norm contractive (#16219)

j-loreaux committed 3 years ago

5ef64261

feat(data/{list, multiset}/basic): generalize `pmap_congr` (#16220)

astrainfinita committed 3 years ago

15c8fdda

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

leanprover-community-bot committed 3 years ago

3b0a5074

feat(algebra/order/floor): lemmas about `int.floor`, `int.ceil`, `int.fract`, `round` (#16158)

ocfnash committed 3 years ago

b059a442

feat(algebra/order/smul): `positivity` extension for `smul` (#16162)

YaelDillies committed 3 years ago

4ed5f0e1

feat(data/zmod/quotient): Version of `order_eq_card_zpowers` in terms of `nat.card` without a `fintype`/`finite` assumption (#16175)

tb65536 committed 3 years ago

3d0bb870

feat(topology/uniform_space/uniform_convergence): tendsto_uniformly_on_filter (#15871)

khwilson committed 3 years ago

b6258037

docs(algebra/field/basic): fix typo (#16241)

jcommelin committed 3 years ago

36e16da1

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

leanprover-community-bot committed 3 years ago

b6931e1c

feat(tactic/tauto): add support for `¬_ ≠ _` (#16232)

adomani committed 3 years ago

c5be877a

chore(analysis/normed_space/star/*): migrate use of `a ∈ self_adjoint A` to `is_self_adjoint a` (#16212)

j-loreaux committed 3 years ago

fec8ffec

feat(analysis/convex/cone): add `inner_dual_cone_of_inner_dual_cone_eq_self` for nonempty, closed, convex cones (#15637)

apurvnakade committed 3 years ago

42d64072

feat(algebra/group_with_zero): add `eq_on_inv₀` (#16222)

urkud committed 3 years ago

bd12701e

chore(algebra/order/{module, smul}): Move to the correct spot (#16131)

YaelDillies committed 3 years ago

2ca1b571

refactor(order/well_founded_set): golf, review API (#11303)

urkud committed 3 years ago

4b440bb0

feat(geometry/euclidean/oriented_angle): angles equal to 0 or π (#16229)

jsm28 committed 3 years ago

f1f166b2

feat(topology/separation): add `eq_on_closure₂` (#16206)

urkud committed 3 years ago

a51c2fd2

refactor(algebra/order/{monoid_lemmas_zero_lt + ring} + crumbs) remove duplicate lemmas (#16189)

adomani committed 3 years ago

62740866

feat(category_theory/strong_epi): various results about strong_epi (#16182)

joelriou committed 3 years ago

093c5036

split(analysis/normed/group/seminorm): Split off `analysis.seminorm` (#16152)

YaelDillies committed 3 years ago

f5afe205