leanprover-community/mathlib3

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into GroupModule

kim-em committed 4 years ago

f6d13e81

feat(measure_theory/measure/vector_measure): add `absolutely_continuous.add` and `absolutely_continuous.smul` (#9086)

kex-y committed 4 years ago

49cf3869

feat(linear_algebra/matrix): `M` maps some `v ≠ 0` to zero iff `det M = 0` (#9041)

Vierkantor committed 4 years ago

87e7a0c7

feat(linear_algebra/matrix): some bounds on the determinant of matrices (#9029)

Vierkantor committed 4 years ago

ab0a2959

lint(testing/slim_check/*): break long lines (#9091)

YaelDillies committed 4 years ago

4222c322

feat(data/polynomial/hasse_deriv): Hasse derivatives (#8998)

jcommelin committed 4 years ago

56a59d3e

feat(ring_theory/discrete_valuation_ring): is_Hausdorff (#8994)

jcommelin committed 4 years ago

42dda89e

feat(algebra/module/ordered): simple `smul` lemmas (#9077)

YaelDillies committed 4 years ago

f4f1cd3f

feat(analysis/normed_space/operator_norm): variants of continuous_linear_map.lsmul and their properties (#8984)

RemyDegenne committed 4 years ago

76ab749e

feat(measure_theory/group/arithmetic): add more to_additive attributes for actions (#9032)

alexjbest committed 4 years ago

146dddc3

feat(data/(fin)set/basic): `image` and `mem` lemmas (#9031)

YaelDillies committed 4 years ago

99b70d9e

chore(linear_algebra/affine_space/independent): allow dot notation on affine_independent (#8974)

YaelDillies committed 4 years ago

3d31c2dd

feat(group_theory/group_action): Extract a smaller typeclass out of `mul_semiring_action` (#8918)

eric-wieser committed 4 years ago

7a2ccb6a

feat(analysis/normed_space/inner_product): reflections API (#8884)

hrmacbeth committed 4 years ago

4c7d95fb

chore(*): remove instance binders in exists, for mathport (#9083)

kim-em committed 4 years ago

71df310f

feat(linear_algebra/affine_space/independent): homotheties preserve affine independence (#9070)

ocfnash committed 4 years ago

31081533

feat(ring_theory): `map f (span s) = span (f '' s)` (#9068)

Vierkantor committed 4 years ago

e4e07eab

feat(field_theory/separable): a finite field extension in char 0 is separable (#9066)

Vierkantor committed 4 years ago

aae2b371

feat(ring_theory): PIDs are Dedekind domains (#9063)

Vierkantor committed 4 years ago

157e99d0

feat(analysis/convex/basic): the affine image of the convex hull is the convex hull of the affine image (#9057)

ocfnash committed 4 years ago

c3f2c237

chore(topology/order): relate Sup and Inf of topologies to `generate_from` (#9045)

hrmacbeth committed 4 years ago

57a0789b

feat(algebra/module/basic): add `module.to_add_monoid_End` (#8968)

eric-wieser committed 4 years ago

a8c5c5a5

feat(algebra/subalgebra): add missing actions by and on subalgebras (#9081)

eric-wieser committed 4 years ago

4e8d9666

feat(data/finset): monotone maps preserve the maximum of a finset (#9035)

Vierkantor committed 4 years ago

585c5add

feat(topology/algebra/ordered): `{prod,pi}.order_closed_topology` (#9073)

urkud committed 4 years ago

fc75aea8

feat(linear_algebra/finite_dimensional): make finite_dimensional_bot an instance (#9053)

kim-em committed 4 years ago

8341d165

feat(data/equiv/derangements/basic): define derangements (#7526)

HenrySwanson committed 4 years ago

b4a88e2e

feat(data/nat/enat): refactor coe from nat to enat (#9023)

jcommelin committed 4 years ago

189fe5bd

feat(ring_theory/noetherian): is_noetherian_of_range_eq_ker (#8988)

ChrisHughes24 committed 4 years ago

cef862d7

feat(group_theory/index): define the index of a subgroup (#8971)

tb65536 committed 4 years ago

4dc96e4a

Older