leanprover-community/mathlib3

Pull Requests Commits

feat(data/list/zip): distributive lemmas (#7312)

pechersky committed 4 years ago

1e1e93a2

awainverse committed 4 years ago

c0ee1106

awainverse committed 4 years ago

02762807

feat(src/group_theory/subgroup): add closure.submonoid.closure (#7328)

riccardobrasca committed 4 years ago

b401f074

feat(data/nat/gcd, ring_theory/int/basic): add some basic lemmas (#7314)

Ruben-VandeVelde committed 4 years ago

aff758ee

chore(computability/language): golf some proofs (#7301)

urkud committed 4 years ago

f8464e35

feat(data/list/nodup): nodup.ne_singleton_iff (#7298)

pechersky committed 4 years ago

0521e2ba

feat(algebra/big_operators): `prod_ite_of_{true, false}`. (#7291)

ericrbg committed 4 years ago

1c07dc0e

feat(data/list): suffix_cons_iff (#7287)

b-mehta committed 4 years ago

a104211d

feat(algebra/lie/tensor_product): define (binary) tensor product of Lie modules (#7266)

ocfnash committed 4 years ago

98ccc666

feat(set/lattice): nonempty_of_union_eq_top_of_nonempty (#7254)

kim-em committed 4 years ago

fa49a635

feat(group_theory/perm/*): Generating S_n (#7211)

tb65536 committed 4 years ago

1585b14a

refactor(algebra/big_operators/finprod) move finiteness assumptions to be final parameters (#7196)

apnelson1 committed 4 years ago

69297401

feat(algebra/lie/nilpotent): basic lemmas about nilpotency (#7181)

ocfnash committed 4 years ago

a1f3ff85

feat(algebra/monoid_algebra): add mem.span_support (#7323)

riccardobrasca committed 4 years ago

a28012c8

feat(algebra/group_power/basic): `pow_ne_zero_iff` and `pow_pos_iff` (#7307)

benjamindavidson committed 4 years ago

3d2fec5f

feat(category_theory/adjunction): reflective adjunction induces partial bijection (#7286)

b-mehta committed 4 years ago

1f65e42e

chore(data/set/intervals/image_preimage): remove unnecessary add_comm in lemmas (#7276)

kim-em committed 4 years ago

e5e0ae74

feat(analysis/special_functions/exp_log): `continuous_on_exp`/`pow` (#7243)

benjamindavidson committed 4 years ago

56bedb40

refactor(algebra/ring_quot.lean): make ring_quot irreducible (#7120)

sgouezel committed 4 years ago

918aea72

fix(.github/workflows): missing closing parentheses in add_label_from_*.yml (#7320)

bryangingechen committed 4 years ago

5ac093c9

feat(data/fin): help `simp` reduce expressions containing `fin.succ_above` (#7308)

Vierkantor committed 4 years ago

2deda90e

fix(data/finset/lattice): sup'/inf' docstring (#7281)

agjftucker committed 4 years ago

8b7014b9

feat(set_theory/surreal): add ordered_add_comm_group instance for surreal numbers (#7270)

apurvnakade committed 4 years ago

8c05ff87

feat(topology/continuous_function): lemmas about pointwise sup/inf (#7249)

kim-em committed 4 years ago

96d57306

chore(category_theory): replace has_hom with quiver (#7151)

kim-em committed 4 years ago

4591eb5c

refactor(geometry/manifold): redefine some instances (#7124)

urkud committed 4 years ago

8830a20f

doc(data/finset/basic): fix confusing typo (#7315)

ericrbg committed 4 years ago

767d248b

feat(topology/subset_properties): variant of elim_nhds_subcover for compact_space (#7304)

kim-em committed 4 years ago

3fb9823d

feat(data/finset/basic): list.to_finset on list ops (#7297)

pechersky committed 4 years ago

b3b74f89

Newer Older