Commits leanprover-community/mathlib3

chore(topology/omega_complete_partial_order): golf (#11250)

urkud committed 4 years ago

a5807271

feat(data/fintype/basic): `set_fintype_card_eq_univ_iff` (#11244)

tb65536 committed 4 years ago

802f23cf

feat(data/{fin/vec_notation, matrix/notation}): `cons_{add,sub,dot_product}_cons` (#11241)

eric-wieser committed 4 years ago

b27e33a0

feat(linear_algebra/orientation): bases from orientations (#11234)

jsm28 committed 4 years ago

98b64f49

feat(analysis/complex): `re`, `im`, and `closure`/`interior`/`frontier` (#11215)

urkud committed 4 years ago

33b5d264

feat(ring_theory/non_zero_divisors): mul_{left,right}_cancel API (#11211)

pechersky committed 4 years ago

3115ced1

chore(data/nat/prime): reuse a result from algebra.big_operators.associated (#11143)

Ruben-VandeVelde committed 4 years ago

3bd2044b

chore(group_theory/sub{monoid,group}, linear_algebra/basic): rename equivalences to mapped subobjects (#11075)

eric-wieser committed 4 years ago

57a9f8be

feat(linear_algebra/clifford_algebra/equivs): There is a clifford algebra isomorphic to the dual numbers (#10730)

eric-wieser committed 4 years ago

7e5eebd7

chore(group_theory/group_action/defs): add instances to copy statements about left actions to right actions when the two are equal (#10949)

eric-wieser committed 4 years ago

cef32586

chore(measure_theory/measurable_space): use implicit measurable_space argument (#11230)

RemyDegenne committed 4 years ago

8d5830e6

chore(analysis/inner_product_space/basic): extract common `variables` (#11214)

hrmacbeth committed 4 years ago

4912740a

feat(algebra/ring/basic): Introduce non-unital, non-associative rings (#11124)

mans0954 committed 4 years ago

b72d2ab2

chore(algebra/group/pi): `pow_apply` can be `rfl` (#11249)

urkud committed 4 years ago

58b1429a

feat(measure_theory/measure/finite_measure_weak_convergence): add definition and lemmas of pairing measures with nonnegative continuous test functions. (#9430)

kkytola committed 4 years ago

4093834b

fix(algebra/group/type_tags): resolve an instance diamond caused by over-eager unfolding (#11240)

eric-wieser committed 4 years ago

5c8243f9

chore(ring_theory/localization): fix typo in module docstring (#11245)

pechersky committed 4 years ago

862854ed

chore(.github): include co-author attributions in PR template (#11239)

robertylewis committed 4 years ago

dc352a64

chore(analysis/inner_product_space/basic): adjust decidability assumptions (#11212)

hrmacbeth committed 4 years ago

692b6b7c

chore(data/fintype/basic): set.to_finset_univ generalization (#11174)

kmill committed 4 years ago

49cbce22

feat(probability_theory/stopping): define stopped process (#10851)

kex-y committed 4 years ago

037147ec

chore(data/polynomial, data/finset/lattice): basic lemmas (#11237)

eric-wieser committed 4 years ago

5df2e7bb

feat(set_theory/ordinal_arithmetic): Proved `add_log_le_log_mul` (#11228)

vihdzp committed 4 years ago

5f3f01f9

feat(tactic/abel): support 0 in group expressions (#11201)

digama0 committed 4 years ago

18330f63

feat(set_theory/ordinal_arithmetic): Proved `dvd_iff_mod_eq_zero` (#11195)

vihdzp committed 4 years ago

b0f2f559

feat(category_theory/limits/filtered_colimits_commute_with_finite_limits): A curried variant of the fact that filtered colimits commute with finite limits. (#11154)

adamtopaz committed 4 years ago

7f244cfe

feat(ring_theory/discriminant): add of_power_basis_eq_norm (#11149)

riccardobrasca committed 4 years ago

06c3ab2b

feat(data/finset): to_finset empty iff (#11088)

b-mehta committed 4 years ago

4a0e844b

feat(testing/slim_check): teach slim_check about `finsupp`s (#10916)

alexjbest committed 4 years ago

68d2d213

chore(*): Rename instances (#9200)

YaelDillies committed 4 years ago

7d42deda