leanprover-community/mathlib

Pull Requests Commits

relax assumption

jjaassoonn committed 3 years ago

7f56ba3b

jjaassoonn committed 3 years ago

468821e8

jjaassoonn committed 3 years ago

a8d8e881

jjaassoonn committed 3 years ago

5de03a15

jjaassoonn committed 3 years ago

8a63a2b2

add mono instance

jjaassoonn committed 3 years ago

7b843ebb

jjaassoonn committed 3 years ago

da10a20a

adopt advice from code review

jjaassoonn committed 3 years ago

f8dd430b

jjaassoonn committed 3 years ago

bcd50850

chore(algebra/ring/basic): postpone unneeded imports (#16863)

kim-em committed 3 years ago

b8d96d77

feat(analysis/seminorm): closed balls for a seminorm (#16676)

ADedecker committed 3 years ago

e71a12cd

feat(order/cover): congr lemmas for `covby` (#15663)

vihdzp committed 3 years ago

a64e3646

feat(category_theory/closed/functor_category): the functor category from a groupoid to a monoidal closed category is monoidal closed (#15643)

antoinelab01 committed 3 years ago

c0e00a87

feat(data/finite/card): Add `finite.card_pos` (#16858)

tb65536 committed 3 years ago

619fd4d5

feat(algebraic_topology): extra degeneracies and homotopy equivalences (#16855)

joelriou committed 3 years ago

324a7502

refactor(ring_theory/class_group): redefine class_group without fraction field (#16727)

Vierkantor committed 3 years ago

d0259b01

feat(linear_algebra/clifford_algebra): the clifford algebra is isomorphic as a module to the exterior algebra (#11468)

eric-wieser committed 3 years ago

446eb51c

feat(topology): accumulation in infinite compact sets. (#16862)

PatrickMassot committed 3 years ago

675192fc

chore(algebra/group/basic): split file (#16847)

kim-em committed 3 years ago

0ff989e5

feat(topology/sheaves/stalks): stalk functor preserves monomorphism (#16797)

jjaassoonn committed 3 years ago

05b820ec

feat(algebra/order/ring): Non-cancellative ordered semirings (#16172)

YaelDillies committed 3 years ago

f5a600f8

feat(data/bool/basic): add `bool.cond_eq_ite` (#16834)

urkud committed 3 years ago

fdb930f3

feat(measure_theory/covering): improve Vitali families and Lebesgue density theorem (#16830)

ocfnash committed 3 years ago

a67fbae6

feat(data/set/prod): add lemmas about `set.pi` (#16828)

urkud committed 3 years ago

f585481b

feat(algebra/module/projective): projective modules are closed under direct sums (#16743)

antoinelab01 committed 3 years ago

666d8787

feat(set_theory/cardinal/ordinal): Beth numbers form a normal family (#16853)

YaelDillies committed 3 years ago

2a528d11

feat(probability/variance): introduce `ℝ≥0∞`-valued variance (#16730)

kex-y committed 3 years ago

85453a2a

feat(group_theory/quotient_group): congr for lifting an isomorphism to group quotients (#16726)

Vierkantor committed 3 years ago

ffd1e5cb

feat(order/atoms): Galois (co)insertions and (co)atoms (#16663)

j-loreaux committed 3 years ago

5d25c8ab

feat(topology/algebra/order/left_right): left and right limits (#16551)

sgouezel committed 3 years ago

052b6cbe

Older