leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 4 years ago

b480385c

chore(computability/regular_expressions): eliminate `finish` (#10811)

stuart-presnell committed 4 years ago

bb51df36

feat(ring_theory/localization,group_theory/monoid_localization): other scalar action instances (#10804)

eric-wieser committed 4 years ago

5658241a

chore(analysis/special_functions/pow): remove duplicate lemmas concerning monotonicity of `rpow` (#10794)

j-loreaux committed 4 years ago

930ae468

doc(linear_algebra/std_basis): update module doc (#10818)

Vierkantor committed 4 years ago

61949afe

doc(undergrad): Link the affine group (#10797)

eric-wieser committed 4 years ago

9f787c2c

feat(data/finsupp/basic): Add `finsupp.erase_of_not_mem_support` (#10689)

stuart-presnell committed 4 years ago

c574e387

chore(data/sym/sym2): Better lemma names (#10801)

YaelDillies committed 4 years ago

03a250a4

chore(algebra/algebra/basic): alg_equiv.map_smul (#10805)

pechersky committed 4 years ago

40cfdecd

docs(undergrad): more links (#10790)

PatrickMassot committed 4 years ago

8f5031ae

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

Older