leanprover-community/mathlib

Pull Requests Commits

feat(data/sign): `sign_one`, `sign_mul`, `sign_pow` (#16058)

jsm28 committed 3 years ago

2230ae61

feat(linear_algebra/ray): relation to linear independence (#16056)

jsm28 committed 3 years ago

9d24857b

feat(category_theory/lifting_properties): adjunctions (#16038)

joelriou committed 3 years ago

24855f46

feat(logic/basic): given two different elements, one of the two is different from a third (#16023)

adomani committed 3 years ago

909cae04

feat(topology/quasi_separated): Define quasi-separated topological spaces. (#15999)

erdOne committed 3 years ago

33261fbe

feat(category_theory): compute subobjects of structured arrows (#15912)

TwoFX committed 3 years ago

3e0dd193

refactor(analysis/normed_space/pi_Lp): make argument of pi_Lp a term of ℝ≥0∞ instead of ℝ (#15833)

j-loreaux committed 3 years ago

e6f3561b

feat(ring_theory/etale): Localization and formally etale homomorphisms. (#15813)

erdOne committed 3 years ago

8a2d93a0

feat(combinatorics/simple_graph): add three useful lemmas relating walk.support and walk.append (#15687)

bottine committed 3 years ago

cdb7af2f

feat(analysis/seminorm): Group seminorms (#15594)

YaelDillies committed 3 years ago

fb1787b1

refactor(analysis/inner_product_space): rename `is_self_adjoint` to `is_symmetric` and add `is_self_adjoint` (#15326)

mcdoll committed 3 years ago

5c91a35b

feat(ring_theory/polynomial/vieta): add version of prod_X_add_C_eq_sum_esymm for multiset (#15008)

xroblot committed 3 years ago

05d8b4f3

feat(topology/uniform_space/uniform_convergence_topology): continuity of [pre,post]composition, and other topological properties (#14534)

ADedecker committed 3 years ago

f1e5c657

feat(algebraic_geometry/*): Preliminary lemmas for #16059 (#16060)

erdOne committed 3 years ago

34b2a989

feat(topology/algebra/uniform_group): add instance `topological_group_is_uniform_of_compact_space` (#16027)

ocfnash committed 3 years ago

531db2ef

feat(algebraic/dold_kan): construction of the functors N₁ and N₂ (#16003)

joelriou committed 3 years ago

07d11baa

feat(algebraic_geometry): Being quasi-compact is a local property. (#15995)

erdOne committed 3 years ago

9b298fea

chore(ring_theory/*): make ACC/DCC on rings be defeq to module versions (#15989)

ericrbg committed 3 years ago

13482743

feat(algebra/group_with_zero): generalize some lemmas (#15985)

urkud committed 3 years ago

9e25db49

chore(combinatorics/*): Fix lint (#16031)

YaelDillies committed 3 years ago

1e6b748c

chore(topology/*): Fix lint (#16030)

YaelDillies committed 3 years ago

1ec48762

feat(combinatorics/young_diagram): add Young diagrams (#15822)

jakelev committed 3 years ago

8a9a16da

feat(order/bounded_order): with_top.of_dual (#15727)

pechersky committed 3 years ago

091ccfb2

feat(catgory_theory/sites): Image sheaf (#15282)

erdOne committed 3 years ago

75edc28a

feat(group_theory/divisible): definition of divisible group (#15030)

jjaassoonn committed 3 years ago

445154a5

refactor(data/set/basic): Adds `inter_nonempty` to match `union_nonempty`. (#14854)

linesthatinterlace committed 3 years ago

8cd4f196

feat(category_theory/preadditive): inclusion functor from left exact functors to additive functors (#12339)

TwoFX committed 3 years ago

9f5d911e

feat(set/prod): decidable mem instance for diagonal (#15846)

dtumad committed 3 years ago

ed833060

chore(probability/martingale/convergence): fix doc-string (#16062)

kex-y committed 3 years ago

3cf22a91

chore(category_theory/limits): generalize universes for limits in punit (#16050)

TwoFX committed 3 years ago

c85d2ff9

Newer Older