leanprover-community/mathlib3

Pull Requests Commits

jcommelin committed 4 years ago

9517bc6f

chore(ring_theory/roots_of_unity): change argument order (#11415)

ericrbg committed 4 years ago

e6db2457

feat(order,data/set/intervals): lemmas about `is_bot`/`is_top` (#11412)

urkud committed 4 years ago

0c844566

doc(number_theory/cyclotomic/basic): fix docstrings (#11411)

ericrbg committed 4 years ago

3f1ac6c5

feat(combinatorics/configuration): Cardinality results for projective plane. (#11406)

tb65536 committed 4 years ago

e839c9ae

refactor(linear_algebra/affine_space): move def of `slope` to a new file (#11361)

urkud committed 4 years ago

12b6b993

doc(data/pfun): fix a typo (#11410)

urkud committed 4 years ago

3fed75a2

fix(data/equiv/set): Fix doc comment syntax (#11409)

nomeata committed 4 years ago

dfad4c6b

feat(linear_algebra/pi): linear_map.vec_cons and friends (#11343)

eric-wieser committed 4 years ago

1f370bb4

refactor(order/directed): Make `is_directed` a Prop mixin (#11238)

YaelDillies committed 4 years ago

e6fab1dc

feat(combinatorics/configuration): Define projective planes (#11390)

tb65536 committed 4 years ago

2a380976

feat(number_theory/cyclotomic/basic): add cyclotomic_field and cyclotomic_ring (#11383)

riccardobrasca committed 4 years ago

5e48b217

feat(data/mv_polynomial/variables): add mv_polynomial.total_deg_finset_sum (#11375)

Jlh18 committed 4 years ago

fa9d2bf3

fix(order/complete_lattice): fix diamond in sup vs max and min vs inf (#11309)

eric-wieser committed 4 years ago

258686f9

feat(data/nat/factorization): add lemma `factorization_prod` (#11395)

stuart-presnell committed 4 years ago

975031d5

fix(tactic/ring_exp): fix normalization proof of unchanged subexpressions (#11394)

Vierkantor committed 4 years ago

67593dcd

feat(data/sigma/interval): A disjoint sum of locally finite orders is locally finite (#10929)

YaelDillies committed 4 years ago

aece00a2

feat(order/cover): `f a` covers `f b` iff `a` covers `b` (#11392)

YaelDillies committed 4 years ago

e8eb7d96

feat(topology/algebra/continuous_monoid_hom): New file (#11304)

tb65536 committed 4 years ago

912c47d3

feat(analysis/complex/basic): determinant of `conj_lie` (#11389)

jsm28 committed 4 years ago

c1f3f1af

chore(algebra/ring/basic): generalize `is_domain.to_cancel_monoid_with_zero` to `no_zero_divisors` (#11387)

eric-wieser committed 4 years ago

72c86c3f

feat(algebra/order/floor): adds some missing floor API (#11336)

b-mehta committed 4 years ago

cb1b6d97

feat(data/multiset/basic): add map_count_true_eq_filter_card (#11306)

BoltonBailey committed 4 years ago

bfe95158

chore(order/lexicographic): cleanup (#11299)

eric-wieser committed 4 years ago

9fd03e1d

feat(topology/uniform_space/compact_convergence): when the domain is locally compact, compact convergence is just locally uniform convergence (#11292)

ocfnash committed 4 years ago

deac58aa

feat(topology/homotopy/product): Product of homotopic paths (#11153)

prakol16 committed 4 years ago

20997252

feat(data/polynomial/taylor): taylor's formula (#11139)

pechersky committed 4 years ago

15b5e24e

feat(analysis/normed_space/lp_space): API for `lp.single` (#11307)

hrmacbeth committed 4 years ago

af074c84

refactor(topology/algebra/uniform_group): Use `to_additive` (#11366)

tb65536 committed 4 years ago

cdd44cd7

feat(analysis/special_functions/pow): norm_num extension for rpow (#11382)

digama0 committed 4 years ago

89f4786e

Older