leanprover-community/mathlib

Pull Requests Commits

chore(deprecated/group): Swap the import direction with algebra/group_power/basic

eric-wieser committed 5 years ago

83f7ea1a

feat(algebra/module/basic): generalize `is_scalar_tower` instances (#5135)

eric-wieser committed 5 years ago

a8ddd7b2

feat(linear_algebra/*): Use alternating maps for wedge and determinant (#5124)

eric-wieser committed 5 years ago

d6241cb0

feat(number_theory/arithmetic_function): Möbius inversion for `add_comm_group`s, `comm_group`s (#5115)

awainverse committed 5 years ago

61f63649

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

leanprover-community-bot committed 5 years ago

f7e1806d

feat(data/nat/sqrt): add simple inequality lemmas and "no middle square" (#5155)

AdrianDoM committed 5 years ago

c2c7afe9

refactor(*): Add `_injective` alongside `_inj` lemmas (#5150)

eric-wieser committed 5 years ago

9a4ed2aa

chore(category_theory/limits): separate regular and normal monos (#5149)

b-mehta committed 5 years ago

c2b7d237

feat(linear_algebra/multilinear): Add dom_dom_congr (#5136)

eric-wieser committed 5 years ago

6c456e35

feat(category_theory/limits/preserves): preserving equalizers (#5044)

b-mehta committed 5 years ago

41e0903f

chore(algebra/group/basic): Add eq_one_iff_eq_one_of_mul_eq_one (#5169)

eric-wieser committed 5 years ago

2a684774

feat(tactic/ring_exp): handle `nat.succ p` as `p + 1` (#5166)

Vierkantor committed 5 years ago

24596cae

feat(ring_theory/perfection): perfection and tilt (#5032)

kckennylau committed 5 years ago

9e78823c

doc(linear_algebra/determinant): Add a reference to is_basis.det (#5167)

eric-wieser committed 5 years ago

b7649bcd

chore(data/equiv/perm): Move around lemmas about perm and swap (#5153)

eric-wieser committed 5 years ago

c088f657

feat(linear_algebra): Add alternating multilinear maps (#5102)

zhangir-azerbayev committed 5 years ago

7188eae5

feat(rat/{basic,floor}) add floor lemmas (#5148)

kappelmann committed 5 years ago

ca3351f6

feat(algebra/lie/basic): Define lattice structure for `lie_submodule`s (#5146)

Oliver Nash committed 5 years ago

2b074bea

doc(data/mv_polynomial/basic): Fix documentation of mv_polynomial.monomial (#5160)

BoltonBailey committed 5 years ago

a8831524

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

leanprover-community-bot committed 5 years ago

b846aa52

refactor(combinatorics/simple_graph): move simple graph files to their own folder (#5154)

agusakov committed 5 years ago

c3f4d1b8

feat(linear_algebra/determinant): Show that the determinant is a multilinear map (#5142)

eric-wieser committed 5 years ago

e3a699ed

feat(ring_theory/integral_closure): Cleanup interface for ring_hom.is_integral (#5144)

dtumad committed 5 years ago

9f955fe5

feat(category_theory/limits): reflexive coequalizers (#5123)

b-mehta committed 5 years ago

1f1ba587

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

leanprover-community-bot committed 5 years ago

5866812c

feat(tactic/explode): display exploded proofs as widgets (#4718)

minchaowu committed 5 years ago

fe7b407f

chore(group_theory/perm/sign): Add swap_mul_involutive (#5141)

eric-wieser committed 5 years ago

ec822277

feat(category_theory/limits): images, equalizers and pullbacks imply functorial images (#5140)

TwoFX committed 5 years ago

916bf74a

chore(algebra/char_p): refactor char_p (#5132)

kckennylau committed 5 years ago

b1d8b897

feat(analysis/normed_space/dual): Fréchet-Riesz representation for the dual of a Hilbert space (#4379)

dupuisf committed 5 years ago

137163a8

Older