leanprover-community/mathlib3

Pull Requests Commits

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

leanprover-community-bot committed 4 years ago

b9722807

feat(data/int/cast): cast_nat_abs (#8120)

jcommelin committed 4 years ago

0faf0864

feat(topology/vector_bundle): `topological_vector_bundle_core` (#8089)

Nicknamen committed 4 years ago

ad00a021

feat(algebra/free_non_unital_non_assoc_algebra): construction of the free non-unital, non-associative algebra on a type `X` with coefficients in a semiring `R` (#8141)

ocfnash committed 4 years ago

e70093ff

docs(data/string/*): add module docstrings (#8144)

YaelDillies committed 4 years ago

e7131068

feat(algebra/big_operators/basic): nat_abs_sum_le (#8132)

jcommelin committed 4 years ago

8ee29671

feat(data/complex/module): add complex.lift to match zsqrtd.lift (#8107)

eric-wieser committed 4 years ago

3a5851f0

fix(algebra/algebra/subalgebra): fix incorrect namespaces and remove duplicate instance (#8140)

eric-wieser committed 4 years ago

36c90d5e

chore(algebra/algebra): trivial lemmas for alg_equiv (#8139)

eric-wieser committed 4 years ago

d420db54

feat(data/set/basic): range_pair_subset (#8133)

jcommelin committed 4 years ago

9c03c035

feat(algebra/ordered_ring): abs_cases lemma (#8124)

AlexKontorovich committed 4 years ago

1de192f4

feat(linear_algebra/clifford_algebra): two algebras are isomorphic if their quadratic forms are equivalent (#8128)

eric-wieser committed 4 years ago

db059004

docs(data/dlist/basic): add module docstring (#8079)

YaelDillies committed 4 years ago

9a8dcb9b

feat(data/int/basic): int.nat_abs_sub_le (#8118)

jcommelin committed 4 years ago

eeeb2238

feat(algebra/{covariant_and_contravariant + ordered_monoid): add instance, golf, docs (#8067)

adomani committed 4 years ago

af8a38fd

docs(data/char): add module docstring (#8043)

YaelDillies committed 4 years ago

3ee436d2

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

leanprover-community-bot committed 4 years ago

8cacd99e

doc(topology/separation): module + lemma docs (#8091)

ericrbg committed 4 years ago

917bcd44

docs(data/list/sections): add module docstring (#8033)

YaelDillies committed 4 years ago

2600baf0

feat(algebra/to_additive): do not additivize operations on constant types (#7792)

fpvandoorn committed 4 years ago

2c749b12

feat(ring_theory/power_basis): extensionality for algebra homs (#8110)

Vierkantor committed 4 years ago

e6ec9016

feat(analysis/normed_space/inner_product): the orthogonal projection is self adjoint (#8116)

RemyDegenne committed 4 years ago

505c32f5

feat(data/ordmap/ordset): Implement some more `ordset` functions (#8127)

winestone committed 4 years ago

5ecd078d

feat(algebra/ordered_group): add a few instances, prune unneeded code (#8075)

adomani committed 4 years ago

d558350f

feat(topology/continuous_function/stone_weierstrass): complex Stone-Weierstrass (#8012)

hrmacbeth committed 4 years ago

bdf2d81e

feat(data/setoid/partition): indexed partition (#7910)

PatrickMassot committed 4 years ago

4cdfbd25

feat(analysis/normed_space/basic): int.norm_eq_abs (#8117)

jcommelin committed 4 years ago

23ee7ea7

feat(algebra/ordered_group): add instances mixing `group` and `co(ntra)variant` (#8072)

adomani committed 4 years ago

d249e533

feat(group_theory/free_abelian_group_finsupp): isomorphism between `free_abelian_group` and `finsupp` (#8046)

jcommelin committed 4 years ago

70fcf999

chore(analysis/special_functions/pow): versions of tendsto/continuous_at lemmas for (e)nnreal (#8113)

hrmacbeth committed 4 years ago

68d7d001

Newer Older