leanprover-community/mathlib3

Pull Requests Commits

feat(order/compactly_generated): A compactly-generated modular lattice is complemented iff atomistic (#6071)

awainverse committed 4 years ago

030107f6

feat(ring_theory/polynomial/chebyshev/dickson): Introduce generalised Dickson polynomials (#5869)

Julian-Kuelshammer committed 4 years ago

7fb7fb36

feat(analysis/analytic/inverse): convergence of the inverse of a power series (#5854)

sgouezel committed 4 years ago

c70feebd

feat(algebra/subalgebra): Trivial subalgebra has trivial automorphism group (#5672)

tb65536 committed 4 years ago

19f24ced

feat(archive/imo): formalize 1987Q1 (#4731)

urkud committed 4 years ago

983cb905

refactor(data/finset/basic): simplify proof (#6160)

Jesse Michael Han committed 4 years ago

13c9ed34

refactor(ring_theory/perfection): faster proof of `coeff_frobenius` (#6159)

Jesse Michael Han committed 4 years ago

0bc7fc1b

feat(algebra/category/Group/adjunctions): adjunction of abelianization and forgetful functor (#6154)

Julian-Kuelshammer committed 4 years ago

6e52dfe3

feat(linear_algebra/matrix): lemmas for `reindex({_linear,_alg}_equiv)?` (#6153)

Vierkantor committed 4 years ago

bce1cb3e

feat(data/int/basic): an integer of absolute value less than one is zero (#6151)

adomani committed 4 years ago

eca4f38f

feat(data/nat/basic): le_of_add_le_* (#6145)

pechersky committed 4 years ago

14a1fd7b

chore(algebra/module/pi): add missing smul_comm_class instances (#6139)

eric-wieser committed 4 years ago

dbbac3b3

feat(data/polynomial/denoms_clearable): add lemma about clearing denominators in evaluating a polynomial (#6122)

adomani committed 4 years ago

56fde49b

feat(category_theory/differential_object): the shift functor (#6111)

kim-em committed 4 years ago

db0fa613

refactor(combinatorics/simple_graph/basic): change statement of mem_decidable to more general version (#6157)

agusakov committed 4 years ago

f0413daf

feat(data/nat/basic): prove an inequality of natural numbers (#6155)

adomani committed 4 years ago

83118da7

feat(data/polynomial/ring_division): comp_eq_zero_iff (#6147)

tb65536 committed 4 years ago

ca8e0093

feat(field_theory/splitting_field): splits_of_nat_degree_le_one (#6146)

tb65536 committed 4 years ago

41530ae3

feat(algebra/ordered_monoid): min_*_distrib (#6144)

pechersky committed 4 years ago

3fae96c9

feat(linear_algebra/prod): add an ext lemma that recurses into products (#6124)

eric-wieser committed 4 years ago

3cc398b2

feat(topology/constructions): add `map_fst_nhds` and `map_snd_nhds` (#6142)

urkud committed 4 years ago

08545369

feat(analysis/normed_space/operator_norm): bundle more arguments (#6140)

urkud committed 4 years ago

7fd4dcf1

refactor(linear_algebra/basic): extract definitions about pi types to a new file (#6130)

eric-wieser committed 4 years ago

d5e2029d

refactor(data/set/intervals/basic): simpler proof of `Iio_union_Ioo'` (#6132)

Jesse Michael Han committed 4 years ago

7a51c0f6

refactor(order/closure): golf `closure_inter_le` (#6138)

Jesse Michael Han committed 4 years ago

5a2eac67

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

leanprover-community-bot committed 4 years ago

0731a700

chore(group_theory/perm/sign): speed up sign_aux_swap_zero_one proof (#6128)

pechersky committed 4 years ago

922ecb07

chore(data/fin): reorder file to group declarations (#6109)

pechersky committed 4 years ago

18b378d8

feat(data/equiv/mul_add): monoids/rings with one element are isomorphic (#6079)

kbuzzard committed 4 years ago

4c1c11ce

feat(algebra/geom_sum): adds further variants (#6077)

Julian-Kuelshammer committed 4 years ago

b34da002

Newer Older