leanprover-community/mathlib

Pull Requests Commits

feat(logic/basic): add two simp lemmas (#8148)

fpvandoorn committed 4 years ago

6e0d2d3b

chore(linear_algebra/matrix/determinant): squeeze some simps for speed up (#8156)

adomani committed 4 years ago

8986c4fd

feat(logic/basic): subtype.subsingleton (#8138)

jcommelin committed 4 years ago

582ee9ee

feat(order/preorder_hom): preorder_hom_eq_id (#8135)

jcommelin committed 4 years ago

aabb900b

feat(category_theory/limits/concrete_category): Some lemmas about limits in concrete categories (#8130)

adamtopaz committed 4 years ago

4a758765

feat(data/int/basic): int.eq_zero_of_div_eq_zero (#8134)

jcommelin committed 4 years ago

2df573a5

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

Newer Older