leanprover-community/mathlib

Pull Requests Commits

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

Remove unused args to fix lint error

stuart-presnell committed 3 years ago

b049100a

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

feat(geometry/euclidean/oriented_angle): more on relation to unoriented angles (#16215)

jsm28 committed 3 years ago

474f96ac

feat(algebra/order): lemmas about `cmp` and arithmetic operations (#16207)

urkud committed 3 years ago

9b759111

Add section docstring

stuart-presnell committed 3 years ago

f6ed1260

stuart-presnell committed 3 years ago

ff25e39e

Change var in `factorization_eq_of_lt_factorization_add`

stuart-presnell committed 3 years ago

a6452149

feat(topology/sheaves/sheaf_condition/opens_le_cover): generalize universe (#16214)

alreadydone committed 3 years ago

7362d50a

refactor(category_theory/morphism_property): stable_under_base_change (#16196)

joelriou committed 3 years ago

912a310a

feat(analysis/normed_space/basic): if `E` is a `normed_space` over `ℚ` then `ℤ ∙ e` is discrete for any `e` in `E` (#16135)

ocfnash committed 3 years ago

53b79573

refactor(field_theory/*): Move and golf `alg_hom.fintype` (#16114)

tb65536 committed 3 years ago

214f197b

feat(algebraic_geometry/limits): Empty scheme is initial. (#16086)

erdOne committed 3 years ago

7f06271e

feat(algebra/order/floor): `floor`/`ceil` are preserved under order ring homs (#16025)

YaelDillies committed 3 years ago

fa0bbc79

refactor(algebraic_geometry/*): Make `LocallyRingedSpace.hom` a custom structure. (#15973)

erdOne committed 3 years ago

a9402e0a

feat(ring_theory/localization/away): finitely presented as R[X]/(rX-1) (#12455)

alreadydone committed 3 years ago

94f13c65

chore(algebra/order/with_zero): Move unrelated lemmas (#15676)

YaelDillies committed 3 years ago

44de64f1

feat(analysis/complex/arg): `same_ray_iff_arg_div_eq_zero` (#16218)

jsm28 committed 3 years ago

6cc2de23

feat(data/seq/seq): prove `seq.ext` earlier (#15830)

vihdzp committed 3 years ago

757e73c5

feat(group_theory/index): `card_dvd_of_surjective` (#16133)

tb65536 committed 3 years ago

04763f32

`factorization_sub_of_lt'` & `factorization_sub_min`

stuart-presnell committed 3 years ago

b454d890

Add section docstring

stuart-presnell committed 3 years ago

616a26cb

Add `factorization_add`

stuart-presnell committed 3 years ago

c7c14ae3

chore(algebra/algebra/spectrum): generalize some spectrum results from `alg_hom` to `alg_hom_class` (#16177)

j-loreaux committed 3 years ago

6f1ad825

Newer Older