leanprover-community/mathlib

Pull Requests Commits

urkud committed 4 years ago

f3ea6780

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

feat(number_theory): define "admissible" absolute values (#8964)

Vierkantor committed 4 years ago

ded0d640

feat(data/finset): define `finset.pimage` (#8907)

urkud committed 4 years ago

ec514603

chore(linear_algebra/basic): speed up slow decl (#9060)

jcommelin committed 4 years ago

628969b1

chore(scripts): update nolints.txt (#9079)

leanprover-community-bot committed 4 years ago

782a20a2

feat(algebra/algebra): lemmas connecting `basis ι R A`, `no_zero_smul_divisors R A` and `injective (algebra_map R A)` (#9039)

Vierkantor committed 4 years ago

dcd87822

docs(linear_algebra/bilinear_map): fix inconsistency in docstring (#9075)

jcommelin committed 4 years ago

50f5d8be

Older