Commits leanprover-community/mathlib

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

doc(category_theory/limits/shapes/pullbacks): fix doc (#11225)

ericrbg committed 4 years ago

b99a98e3

feat(topology/fiber_bundle): a topological fiber bundle is a quotient map (#11194)

urkud committed 4 years ago

a30375e0

feat(algebra/opposites): add `add_opposite` (#11080)

urkud committed 4 years ago

aa82ba00

feat(data/finset/sigma): A way to lift `finset`-valued functions to a sigma type (#10958)

YaelDillies committed 4 years ago

a7aa2c87

feat(data/finset/slice): `r`-sets and slice (#10685)

YaelDillies committed 4 years ago

8bd20598

feat(analysis/inner_product_space/dual,adjoint): add some lemmas about extensionality with respect to a basis (#11176)

dupuisf committed 4 years ago

1aec9a19

feat(*): Prerequisites for the Spec gamma adjunction (#11209)

erdOne committed 4 years ago

03872fdd