leanprover-community/mathlib

Pull Requests Commits

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

Start `factorization_add_iff`; golf `factorization_add_of_lt`

stuart-presnell committed 3 years ago

1510b706

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

Extract `factorization_add_le_of_factorization_add_eq`

stuart-presnell committed 3 years ago

ce239945

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

stuart-presnell committed 3 years ago

c2557da6

stuart-presnell committed 3 years ago

b5bfaf4d

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

First proof of `factorization_sub`

stuart-presnell committed 3 years ago

f9406225

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

YaelDillies committed 3 years ago

f5afe205

feat(data/polynomial/module): Some api for `polynomial_module`. (#16126)

erdOne committed 3 years ago

81afa2cb

feat(algebraic_topology/dold_kan): the normalized Moore complex is a direct factor of the alternating face map complex (#16071)

joelriou committed 3 years ago

fc5b2d2e

Newer Older