leanprover-community/mathlib3

Pull Requests Commits

kbuzzard committed 3 years ago

94c465be

Merge branch 'master' into kbuzzard-pid-unique1

kbuzzard committed 3 years ago

9215aa2d

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

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

feat(category_theory/currying): bifunctor version of whiskering_right (#15504)

antoinelab01 committed 3 years ago

0be7214f

feat(order/heyting_algebra): Heyting algebras (#15305)

YaelDillies committed 3 years ago

96ed4226

feat(algebra/category): forgetful functors from modules/abelian groups preserve epis/monos (#15108)

TwoFX committed 3 years ago

4e64a3fa

feat(analysis/special_functions/trigonometric/angle): continuity and signs (#16204)

jsm28 committed 3 years ago

40427f78

feat(algebra/order/monoid): a canonically ordered add monoid has `0 ≤ 1` (#16199)

urkud committed 3 years ago

730cde34

Older