leanprover-community/mathlib3

Pull Requests Commits

jjaassoonn committed 3 years ago

561c41db

does this fix universe error?

jjaassoonn committed 3 years ago

4518f580

fix no_inhbaited

jjaassoonn committed 3 years ago

3b2a72d5

jjaassoonn committed 3 years ago

174f372f

Merge remote-tracking branch 'origin/master' into bundled_module

jjaassoonn committed 3 years ago

8c26edaf

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

feat(order/category/HeytAlg): The category of Heyting algebras (#16250)

YaelDillies committed 3 years ago

51cbe888

feat(linear_algebra/matrix/charpoly) Generalize Cayley-Hamilton theorem. (#15105)

erdOne committed 3 years ago

46146be0

feat(topology/continuous_on): generalise lemma slightly (#16840)

b-mehta committed 3 years ago

90fab282

chore(data/pfunctor/univariate): remove use of `h_generalize` (#16839)

alexjbest committed 3 years ago

827f0b99

Older