leanprover-community/mathlib3

Pull Requests Commits

feat(ring_theory/valuation): definition and basic properties of valuations (#3222)

jcommelin committed 5 years ago

e68503ad

chore(algebra/group_with_zero): nolint (#3254)

bryangingechen committed 5 years ago

a22cd4d7

chore(scripts): update nolints.txt (#3253)

leanprover-community-bot committed 5 years ago

859edfb0

feat(data/matrix): std_basis_matrix (#3244)

kim-em committed 5 years ago

89f3bbc2

feat(category_theory/limits/shapes): simp lemmas to decompose pullback_cone.mk.fst (#3249)

b-mehta committed 5 years ago

a40be987

chore(topology/*): use dot syntax for some lemmas (#3251)

urkud committed 5 years ago

06256910

feat(algebra/lie_algebra): conjugation transformation for Lie algebras of skew-adjoint endomorphims, matrices (#3229)

Oliver Nash committed 5 years ago

b3915636

chore(ring_theory/polynomial): move `ring_theory.polynomial` to `ring_theory.polynomial.basic` (#3248)

Vierkantor committed 5 years ago

ea961f76

feat(topology): real.image_Icc (#3224)

PatrickMassot committed 5 years ago

9524dee3

fix(tactic/interactive_expr): show let-values in tactic state widget (#3228)

gebner committed 5 years ago

1bc6ebaa

fix(tactic/apply_fun): beta reduction was too aggressive (#3214)

kim-em committed 5 years ago

b82ed0c5

chore(topology/algebra/ordered): use `continuous_at`, rename (#3231)

urkud committed 5 years ago

6d0f40a6

refactor(linear_algebra/affine_space): allow empty affine subspaces (#3219)

jsm28 committed 5 years ago

a143c386

feat(category/schur): a small corollary of the baby schur's lemma (#3239)

kim-em committed 5 years ago

e250eb41

chore(data/set/intervals): split `I??_union_I??_eq_I??` (#3237)

urkud committed 5 years ago

d788d4b5

chore(algebra/ring): move some classes to `group_with_zero` (#3232)

urkud committed 5 years ago

af53c9d7

chore(data/polynomial): partial move from is_ring_hom to ring_hom (#3213)

kim-em committed 5 years ago

da481e77

feat(data/fintype/basic): card_eq_zero_equiv_equiv_pempty (#3238)

kim-em committed 5 years ago

38904ac8

feat(category_theory): remove nearly all universe annotations (#3221)

kim-em committed 5 years ago

1588d81e

perf(linarith): don't repeat nonneg proofs for nat-to-int casts (#3226)

robertylewis committed 5 years ago

056a72aa

feat(analysis/normed_space/real_inner_product,geometry/euclidean): inner products of weighted subtractions (#3203)

jsm28 committed 5 years ago

791744b0

chore(*): import expression widgets from core (#3181)

gebner committed 5 years ago

4fcd6fd4

chore(scripts): update nolints.txt (#3234)

leanprover-community-bot committed 5 years ago

e8fd085f

chore(*): change notation for `set.compl` (#3212)

urkud committed 5 years ago

45904fba

chore(init_/): remove this directory (#3227)

urkud committed 5 years ago

d3006bad

feat(order/filter/germ): define `filter.germ` (#3172)

urkud committed 5 years ago

eb05a940

feat(algebra/ring): ite_mul_one and ite_mul_zero_... (#3217)

kim-em committed 5 years ago

4907d5d6

feat(data/polynomial): work over noncommutative rings where possible (#3193)

kim-em committed 5 years ago

964f0e53

feat(category/limits/shapes): fix biproducts (#3175)

kim-em committed 5 years ago

a708f854

feat(linear_algebra/affine_space): affine independence (#3140)

jsm28 committed 5 years ago

78beab4f

Newer Older