leanprover-community/mathlib

Pull Requests Commits

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

its not working :(

winston-h-zhang committed 4 years ago

056fad73

winston-h-zhang committed 4 years ago

888d8a51

winston-h-zhang committed 4 years ago

91b3e9aa

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

feat(measure_theory/lp_space): add snorm_eq_lintegral_rpow_nnnorm (#8115)

RemyDegenne committed 4 years ago

54eccb0e

feat(algebra/monoid_algebra): adjointness for the functor `G ↦ monoid_algebra k G` when `G` carries only `has_mul` (#7932)

ocfnash committed 4 years ago

90d2046b

feat(algebraic_topology/simplex_category): epi and monos in the simplex category (#8101)

robin-carlier committed 4 years ago

d521b2bc

chore(category_theory/opposites): make hom explicit in lemmas (#8088)

jcommelin committed 4 years ago

07f1235d

Newer Older