leanprover-community/mathlib

Pull Requests Commits

vihdzp committed 2 years ago

d4d0d28f

vihdzp committed 2 years ago

46feb63e

vihdzp committed 2 years ago

8f358536

feat(ring_theory/ideal/norm): add ideal.finite_set_of_abs_norm_eq (#18569)

xroblot committed 2 years ago

d3acee0d

feat(set_theory/zfc/ordinal): more lemmas on transitive sets (#18307)

vihdzp committed 2 years ago

98bbc352

refactor(data/seq): scope seq and wseq to namespace stream (#18284)

arienmalec committed 2 years ago

a7e36e48

chore(scripts/list-attributes.sh): script to track attributes semireducible/irreducible (#18165)

jcommelin committed 2 years ago

95127066

feat(order/upper_lower/locally_finite): Upper closure preserves finiteness (#18678)

YaelDillies committed 2 years ago

3e175454

refactor(category_theory/shift): improve automation (#18670)

joelriou committed 2 years ago

6876fa15

chore(order/category): Rename categories (#18657)

YaelDillies committed 2 years ago

e8ac6315

feat(geometry/manifold/vector_bundle/tangent): use the new tangent bundle definition in the library (#18601)

fpvandoorn committed 2 years ago

01876449

feat(combinatorics/simple_graph/connected): support of connected components (#18442)

bottine committed 2 years ago

b99e2d58

feat(algebraic_topology/dold_kan): tools for compatibilities (#17922)

joelriou committed 2 years ago

160f568d

chore(category_theory/adjunction/opposites): backport removal of simp lemmas (#18680)

kim-em committed 2 years ago

0148d455

feat(set_theory/zfc/basic): simpler/more general `Class.ext` (#18306)

vihdzp committed 2 years ago

ef5f2ce9

chore(analysis/locally_convex/with_seminorms): remove unnecessary positivity assumption (#18659)

mcdoll committed 2 years ago

b31173ee

feat(algebra/order/monoid/min_max): `a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂` (#18667)

YaelDillies committed 2 years ago

de87d505

feat(archive/imo/imo2006_q5): IMO 2006 Q5 (#15613)

vihdzp committed 2 years ago

728baa2f

refactor(topology/algebra/module/strong_topology): split of local convexity (#18671)

mcdoll committed 2 years ago

b8627dba

feat(ring_theory/complex): trace and norm of a complex number (#18658)

eric-wieser committed 2 years ago

9015c511

feat(ring_theory/trace): trace of product rings (#18656)

eric-wieser committed 2 years ago

b68f3403

feat(data/zmod/basic): `zmod.val_min_abs` lemmas (#18119)

javra committed 2 years ago

f209a5a9

feat(representation_theory/group_cohomology_resolution): add isomorphism with nth inhomogeneous cochains (#18159)

Amelia Livingston committed 2 years ago

3dec44d0

feat(set_theory/zfc/basic): tweak Class hom lemmas (#18295)

vihdzp committed 2 years ago

c5dd9310

feat(analysis/locally_convex/with_seminorms): convergence along filters (#18664)

mcdoll committed 2 years ago

ce86f4e0

feat(data/finmap): add an equivalence with pairs `(keys, lookup)` (#18151)

urkud committed 2 years ago

cea83e19

feat(set_theory/ordinal/arithmetic): miscellaneous arithmetic lemmas (#15990)

vihdzp committed 2 years ago

b67044ba

chore(data/set/pairwise): split (#17880)

astrainfinita committed 2 years ago

c227d107

chore(*): Fix mistakes (#18654)

YaelDillies committed 2 years ago

76de8ae0

chore(topology/basic): backport another generalization to `Sort*` (#18660)

urkud committed 2 years ago

e8da5f21

Older