leanprover-community/mathlib3

Pull Requests Commits

feat(logic/function/basic): function.involutive.eq_iff (#7332)

pechersky committed 4 years ago

3a8f9db9

chore(algebra/iterate_hom): generalize `iterate_map_one` and `iterate_map_mul` to mul_one_class (#7331)

eric-wieser committed 4 years ago

15b4fe61

feat(data/matrix/basic): add lemma for assoc of mul_vec w.r.t. smul (#7310)

gabrielmoise committed 4 years ago

4b065bfc

refactor(ring_theory/polynomial/content): Define is_primitive more generally (#7316)

tb65536 committed 4 years ago

6f3d9053

feat(algebra/group/pi): pow_apply (#7302)

kim-em committed 4 years ago

5bd96ce7

refactor(group_theory/submonoid/basic): merge together similar lemmas and definitions (#7280)

eric-wieser committed 4 years ago

85df3a36

feat(algebra/category/Module): mono_iff_injective (#7100)

kim-em committed 4 years ago

0070d22a

feat(algebraic_geometry/Scheme): improve cosmetics of definition (#7325)

kim-em committed 4 years ago

b77916db

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

leanprover-community-bot committed 4 years ago

40bb51e7

chore(geometry/manifold/instances/circle): provide instance (#7333)

kim-em committed 4 years ago

2bd09f0f

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

pechersky committed 4 years ago

1e1e93a2

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

Newer Older