leanprover-community/mathlib3

Pull Requests Commits

`injective.group_div` ensures the division is defeq to the existing `has_div` instance

Vierkantor committed 5 years ago

16d04da2

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

Some more fixes

Vierkantor committed 5 years ago

dd65ba5b

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

Vierkantor committed 5 years ago

b96c3ce1

Merge remote-tracking branch 'mathlib/staging' into bundle_has_sub_div

Vierkantor committed 5 years ago

e4f71c6a

Fix almost all missing `sub_eq_add_neg`s

Vierkantor committed 5 years ago

a7ab4ce5

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

Newer Older