leanprover-community/mathlib

Pull Requests Commits

Wrap in section to control typeclass instances

stuart-presnell committed 4 years ago

20f3e95b

Template for `prod_eq_zero_iff` and `prod_ne_zero_iff`

stuart-presnell committed 4 years ago

0fa056d7

feat(measure_theory/integral/set_to_l1): various properties of the set_to_fun construction (#10713)

RemyDegenne committed 4 years ago

e3eb0eb0

feat(algebraic_geometry): LocallyRingedSpace has coproducts. (#10665)

erdOne committed 4 years ago

1367c19b

feat(algebra/group): make `map_[z]pow` generic in `monoid_hom_class` (#10749)

Vierkantor committed 4 years ago

9078914e

chore(data/equiv/ring): inv_fun_eq_symm (#10779)

pechersky committed 4 years ago

f46a7a0f

feat(combinatorics/simple_graph): simp lemmas about spanning coe (#10778)

b-mehta committed 4 years ago

6d15ea43

feat(group_theory/order_of_element): additivize (#10766)

ericrbg committed 4 years ago

05d87671

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

Older