leanprover-community/mathlib

Pull Requests Commits

feat(combinatorics/additive/salem_spencer): Salem-Spencer sets and Roth numbers (#10509)

YaelDillies committed 4 years ago

108eb0b2

feat(ring_theory/unique_factorization_domain): add count lemmas (#10475)

mariainesdff committed 4 years ago

e1747364

feat(ring_theory/graded_algebra): `homogeneous_element` (#10118)

jjaassoonn committed 4 years ago

efbbb767

feat(linear_algebra/determinant): determinant of a linear equivalence as a unit (#10751)

eric-wieser committed 4 years ago

1589c7b4

chore(order): rename `preorder_hom` to `order_hom` (#10750)

Vierkantor committed 4 years ago

324a605f

refactor(set_theory/ordinal_arithmetic) Separate `is_normal.lt_iff` (#10745)

vihdzp committed 4 years ago

35cd7c0c

feat(analysis/special_function/integrals): integral of `x ^ r`, `r : ℝ`, and `x ^ n`, `n : ℤ` (#10650)

urkud committed 4 years ago

7697ec6e

feat(algebra/order/floor): Floor of `a / n` and other lemmas (#10748)

YaelDillies committed 4 years ago

779517b6

chore(topology/maps): golf, use section vars (#10747)

urkud committed 4 years ago

563c3643

feat(archive/imo): IMO 2005 problem 4 (modular arithmetic) (#10746)

hrmacbeth committed 4 years ago

10fb7f91

split(data/set/prod): split off `data.set.basic` (#10739)

YaelDillies committed 4 years ago

9d73418c

feat(linear_algebra/orientation): inherit an action by `units R` on `module.ray R M` (#10738)

eric-wieser committed 4 years ago

e60899c5

refactor(algebra/triv_sq_zero_ext): generalize and cleanup (#10729)

eric-wieser committed 4 years ago

ea88bd61

feat(data/{list, multiset, finset}/range): add range_add (#10706)

BoltonBailey committed 4 years ago

e70e22f2

feat(order/galois_connection): add lt_iff_lt (#10702)

BoltonBailey committed 4 years ago

e4b6b5cc

feat(data/polynomial/degree/definitions): add pow lemmas (#10698)

greysome committed 4 years ago

29fecae5

feat(analysis/convex/basic): lemmas about midpoint and segment (#10682)

ADedecker committed 4 years ago

fb819501

feat(algebra/graded_monoid): dependent products (#10674)

eric-wieser committed 4 years ago

f8171e09

feat(*): Random lemmas about adjoin/span. (#10666)

erdOne committed 4 years ago

309da201

feat(algebra/pointwise): Multiplying a singleton (#10660)

YaelDillies committed 4 years ago

e19473a9

feat(analysis/convex/strict): Strictly convex sets (#10648)

YaelDillies committed 4 years ago

ec48e3b9

feat(ring_theory/polynomial/cyclotomic/*): ɸₙ(1) = 1 (#10483)

ericrbg committed 4 years ago

2d47c1d6

chore(category_theory/limits): Generalize universe for preserving limits (#10736)

erdOne committed 4 years ago

7cd8adb7

feat(algebraic_geometry): An integral scheme is reduced and irreducible (#10733)

erdOne committed 4 years ago

381b9541

feat(data/mv_polynomial/variables): API for mv_polynomial.degree_of (#10646)

isadofschi committed 4 years ago

214a80f3

feat(category_theory/limits): The associativity of pullbacks and pushouts. (#10619)

erdOne committed 4 years ago

8b8f08d0

feat(algebraic_geometry/presheafed_space): Open immersions of presheafed spaces has pullbacks. (#10069)

erdOne committed 4 years ago

b6b47ed5

feat(category_theory/flat_functor): Generalize results into algebraic categories. (#10735)

erdOne committed 4 years ago

fcd0f11c

feat(data/nat/prime): add `prime.dvd_mul_of_dvd_ne` (#10727)

stuart-presnell committed 4 years ago

06905422

feat(algebra/{group,ring}/opposite): `{ring,monoid}_hom.from_opposite` (#10723)

eric-wieser committed 4 years ago

0c248b74

Newer Older