leanprover-community/mathlib3

Pull Requests Commits

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

feat(data/int): absolute values and integers (#9028)

Vierkantor committed 4 years ago

b0b0a24f

chore(data/set/basic): add some simp attrs (#9074)

urkud committed 4 years ago

fd453cf1

feat(linear_algebra/finite_dimensional): generalisations to division_ring (#8822)

kim-em committed 4 years ago

463e7534

chore(ring_theory): typo fix (#9067)

Vierkantor committed 4 years ago

9c886ffb

feat(algebra/tropical/basic): define tropical semiring (#8864)

pechersky committed 4 years ago

f8cfed4d

feat(algebra/big_operators): absolute values and big operators (#9027)

Vierkantor committed 4 years ago

eeb4bb66

Newer Older