leanprover-community/mathlib

Pull Requests Commits

feat(ring_theory): fg_iff_exists_fin_generating_fam (#7343)

PatrickMassot committed 4 years ago

3821d318

feat(linear_algebra): free_of_finite_type_torsion_free (#7341)

PatrickMassot committed 4 years ago

9cc3d80e

refactor(*): kill int multiplication diamonds (#7255)

sgouezel committed 4 years ago

8e4ef23a

feat(order/extension): extend partial order to linear order (#7142)

b-mehta committed 4 years ago

d052c527

chore(algebra/category): remove duplicated proofs (#7349)

TwoFX committed 4 years ago

d5330fe8

feat(data/finsupp): to_multiset symm apply (#7356)

b-mehta committed 4 years ago

6b2bb8a1

feat(data/list/basic): assorted list lemmas (#7296)

pechersky committed 4 years ago

beb694b9

feat(data/list/forall2): defines sublist_forall2 relation (#7165)

awainverse committed 4 years ago

77168704

feat(archive/imo): IMO 2001 Q2 (#7238)

peakpoint committed 4 years ago

2ecd65e6

feat(linear_algebra): Lagrange formulas for expanding `det` along a row or column (#6897)

Vierkantor committed 4 years ago

8f8b194a

feat(group_theory/nielsen_schreier): subgroup of free group is free (#6840)

dwarn committed 4 years ago

f83ae595

refactor(*): rename `semimodule` to `module`, delete typeclasses `module` and `vector_space` (#7322)

Vierkantor committed 4 years ago

46ceb36e

chore(docs/100.yaml): mention "Erdős–Szekeres" by name (#7353)

benjamindavidson committed 4 years ago

f15887a1

feat(data/int/basic): add nat_abs_ne_zero (#7350)

Ruben-VandeVelde committed 4 years ago

767c8c59

feat(group_theory/{perm/cycle_type, specific_groups/alternating_group}): the alternating group is generated by 3-cycles (#6949)

awainverse committed 4 years ago

27cd5c11

feat(topology/algebra): uniform continuity from 0 (#7318)

b-mehta committed 4 years ago

bbd9362d

refactor(field_theory/algebraic_closure): move complex.is_alg_closed (#7344)

kim-em committed 4 years ago

d89f93a9

feat(algebra/star/pi): star operates elementwise on pi types (#7342)

eric-wieser committed 4 years ago

bb2e7f9e

chore(algebra/opposite): add missing `monoid_with_zero` instance (#7339)

eric-wieser committed 4 years ago

a5b5f6c3

feat(analysis/specific_limits): basic ratio test for summability of a nat-indexed family (#7277)

ADedecker committed 4 years ago

6c092955

feat(linear_algebra/tensor_product): characterise range of tensor product of two linear maps (#7340)

ocfnash committed 4 years ago

33ea6980

doc(field_theory/minpoly): improve some doc-strings (#7336)

kim-em committed 4 years ago

227c42d1

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

Newer Older