leanprover-community/mathlib3

Pull Requests Commits

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

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

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

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

j-loreaux committed 3 years ago

6f1ad825

feat(topology/metric_space): Add first countability instances (#15942)

mcdoll committed 3 years ago

cf9eb049

feat(category_theory): functors preserving epis and kernels are exact (#16129)

javra committed 3 years ago

e919421b

feat(topology/algebra/module/character_space): add facts about `character_space.union_zero` (#16209)

j-loreaux committed 3 years ago

02128fe4

feat(analysis/special_functions/trigonometric): add `real.abs_sinh` (#16211)

urkud committed 3 years ago

f089486a

feat(analysis/special_functions/complex/arg): relation to `real.angle.to_real` (#16205)

jsm28 committed 3 years ago

f399d3a3

chore(algebra/algebra/basic): some helper lemmas for linear maps over algebras (#16200)

eric-wieser committed 3 years ago

0abbdc08

chore(*): golfs with rsufficesI (#16197)

ericrbg committed 3 years ago

9bc7dfa6

feat(data/rat/cast): add lemmas, golf (#16194)

urkud committed 3 years ago

aeb7facf

feat(group_theory/subgroup/basic): Add `map_is_commutative` and `comap_injective_is_commutative` (#16109)

tb65536 committed 3 years ago

62ac221e

Newer Older