leanprover-community/mathlib3

Pull Requests Commits

add `zero_lt_one_of_pos`

astrainfinita committed 3 years ago

f4bdf81d

Merge remote-tracking branch 'origin/FR_order_refactor11' into FR_order_refactor14

astrainfinita committed 3 years ago

00a10d59

Update monoid_lemmas_zero_lt.lean

astrainfinita committed 3 years ago

9f0d9676

Merge branch 'master' into FR_order_refactor11

astrainfinita committed 3 years ago

d8dae542

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

chore(data/finset/pi_induction): fix lint (#16224)

urkud committed 3 years ago

63f2525e

refactor(topology/constructions): rename `continuous_subtype_mk` (#16223)

urkud committed 3 years ago

3339976e

feat(data/nat/enat): new file (#16217)

urkud committed 3 years ago

839b92fe

Older