leanprover-community/mathlib

Pull Requests Commits

chore(measure_theory/decomposition/signed_hahn): Fixed a few typos (#10777)

vihdzp committed 4 years ago

85cb4a81

move(algebra/order/lattice_group): Move from `algebra.lattice_ordered_group` (#10763)

YaelDillies committed 4 years ago

f070a69b

chore(logic/basic): tidy `ite` section and misplaced lemmas (#10761)

YaelDillies committed 4 years ago

f727e126

feat(data/mv_polynomial/basic): add `mv_polynomial.support_sum` (#10731)

isadofschi committed 4 years ago

dda8a10a

feat(analysis/inner_product_space/basic): inner product as a (continuous) sesquilinear map (#10684)

dupuisf committed 4 years ago

9af43e4e

feat(data/mv_polynomial/variables): add `mv_polynomial.degree_of_zero` (#10768)

isadofschi committed 4 years ago

f3fa5e3f

feat(number_theory/padics/padic_norm): lemmas (#10765)

ericrbg committed 4 years ago

ee78812f

feat(data/nat/prime): dvd_of_factors_subperm (#10764)

ericrbg committed 4 years ago

9b1a8321

refactor(linear_algebra/orientation): add refl, symm, and trans lemma (#10753)

eric-wieser committed 4 years ago

d9edeea2

feat(order/basic, order/bounded_order): Generalized `preorder` to `has_lt` (#10695)

vihdzp committed 4 years ago

00004975

chore(set_theory/ordinal_arithmetic): simplified proof of `is_normal.le_self` (#10770)

vihdzp committed 4 years ago

32c24f1b

feat(topology/algebra/*, analysis/normed_space/operator_norm): construct bundled {monoid_hom, linear_map} from limits of such maps (#10700)

j-loreaux committed 4 years ago

cd462cda

feat(algebra/triv_sq_zero_ext): universal property (#10754)

eric-wieser committed 4 years ago

77e52484

feat(analysis/convex/simplicial_complex): Simplicial complexes (#9762)

YaelDillies committed 4 years ago

c3391c26

chore(order/hom): rearrange definitions of `order_{hom,iso,embedding}` (#10752)

Vierkantor committed 4 years ago

7181b3af

chore(algebra/algebra/tower): golf ext lemma (#10756)

eric-wieser committed 4 years ago

b351ca98

feat(order/well_founded) Added `strict_mono.id_le_of_wo` (#10732)

vihdzp committed 4 years ago

3b2cf53d

feat(topology/algebra/group): add homeomorph.prod_units (#10725)

mariainesdff committed 4 years ago

c895ddd9

feat(probability_theory/martingale): add super/sub-martingales (#10710)

kex-y committed 4 years ago

ad88a836

feat(algebra/big_operators/finprod): add div lemmas (#10472)

mariainesdff committed 4 years ago

c7e355d3

refactor(data/set/pairwise): Make arguments of `set.pairwise` semi-implicit (#10740)

YaelDillies committed 4 years ago

0c0ee7b0

doc(linear_algebra/finite_dimensional): update doc to new definition (#10758)

riccardobrasca committed 4 years ago

ee8de4cf

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

Newer Older