leanprover-community/mathlib

Pull Requests Commits

bottine committed 2 years ago

2559d225

bottine committed 2 years ago

ea313a08

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

feat(topology/*): add lemmas about `𝓝[⋃ i, s i] a` (#18321)

urkud committed 2 years ago

55d771df

chore(analysis/normed_space/basic): introduce `norm_smul_le` (#18650)

eric-wieser committed 2 years ago

d3af0609

feat(analysis/convex/topology): Closure of an open segment (#18589)

YaelDillies committed 2 years ago

0e3aacdc

feat(data/finset/pointwise): `s ∩ t * s ∪ t ⊆ s * t` (#17961)

YaelDillies committed 2 years ago

517cc149

chore(category_theory/limits/shapes/concrete_category): Delete empty file (#18653)

YaelDillies committed 2 years ago

0ca15f46

chore(*): add mathlib4 synchronization comments (#18646)

leanprover-community-bot committed 2 years ago

cb3ceec8

fix(tactic/ring_exp): `X^(2^3) = X^8` not `X^6` (#18645)

Vierkantor committed 2 years ago

72e87ce0

refactor(analysis/inner_product_space/basic): do not extend normed_add_comm_group (#18583)

eric-wieser committed 2 years ago

46b633fd

fix(*): missing universe polymorphism (#18644)

eric-wieser committed 2 years ago

d11893b4

chore(data/matrix/kronecker): make the `R` argument implicit (#18624)

eric-wieser committed 2 years ago

945bc74e

feat(tactic/linear_combination): allow `linear_combination with { exponent := n }` (#15428)

robertylewis committed 2 years ago

540b766a

chore(*): add mathlib4 synchronization comments (#18642)

leanprover-community-bot committed 2 years ago

97eab485

feat(order/upper_lower/basic): The upper closure is bounded below (#18637)

YaelDillies committed 2 years ago

e9ce88cd

Older