leanprover-community/mathlib3

Pull Requests Commits

chore(topology/path_connected): move `proj_Icc` to a separate file (#5120)

urkud committed 5 years ago

8acd296e

chore(category_theory/limits): golf a proof (#5130)

TwoFX committed 5 years ago

238c58c3

feat(logic/relation): trans_gen closure (#5129)

pechersky committed 5 years ago

ff2aeae9

feat(data/polynomial/eval): eval₂ f x (p * X) = eval₂ f x p * x (#5110)

urkud committed 5 years ago

af7ba87a

chore(order/basic): add `strict_mono_??cr_on.dual` and `dual_right` (#5107)

urkud committed 5 years ago

8e09111f

chore(category_theory/iso): golf and name consistency (#5096)

b-mehta committed 5 years ago

a106102a

feat(linear_algebra/bilinear_form): equivalence with matrices, given a basis (#5095)

Vierkantor committed 5 years ago

d0789503

feat(number_theory/arithmetic_function): Moebius inversion (#5047)

awainverse committed 5 years ago

c06c6169

feat(field_theory): Prove the Galois correspondence (#4786)

tb65536 committed 5 years ago

2bda184a

chore(data/equiv/basic): redefine `set.bij_on.equiv` (#5128)

urkud committed 5 years ago

2f939e93

chore(data/set/function): add 3 trivial lemmas (#5127)

urkud committed 5 years ago

4715d992

chore(data/complex/exponential): golf 2 proofs (#5126)

urkud committed 5 years ago

c1edbdda

doc(data/equiv/basic): improve docstring of `equiv.sum_equiv_sigma_bool` (#5119)

urkud committed 5 years ago

cb9e5cf9

chore(data/pprod): Add pprod.mk.eta (#5114)

eric-wieser committed 5 years ago

d3cc9935

chore(order/rel_iso): add a few lemmas (#5106)

urkud committed 5 years ago

2c5d4a3c

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

leanprover-community-bot committed 5 years ago

1a8089e9

chore(data/sum): Add trivial simp lemmas (#5112)

eric-wieser committed 5 years ago

59717d68

chore(data/equiv/basic): Add comp_swap_eq_update (#5091)

eric-wieser committed 5 years ago

2d476e0e

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

leanprover-community-bot committed 5 years ago

98ebe5a6

chore(logic/function/basic): Add function.update_apply (#5093)

eric-wieser committed 5 years ago

6e301c75

feat(algebra/triv_sq_zero_ext): trivial square-zero extension (#5109)

kckennylau committed 5 years ago

81207e09

chore(data/int/basic): Add int.units_mul_self (#5101)

eric-wieser committed 5 years ago

4265f2c9

chore(data/equiv/basic): Add trivial simp lemma (#5100)

eric-wieser committed 5 years ago

0324935c

fix(algebra/ordered_group): remove workaround (#5103)

kbuzzard committed 5 years ago

00200778

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

leanprover-community-bot committed 5 years ago

83f293e2

fix(algebra/group_with_zero/power): remove duplicate lemmas (#5083)

kbuzzard committed 5 years ago

7e66984c

chore(linear_algebra/multilinear_map): Add boring coercion lemmas copied from ring_hom (#5099)

eric-wieser committed 5 years ago

2ed48468

feat(analysis/special_functions/trigonometric): sin, cos, sinh, and cosh are infinitely smooth (#5090)

urkud committed 5 years ago

943b1294

chore(group_theory/perm/sign): Golf another proof

eric-wieser committed 5 years ago

eb5e3862

chore(group_theory/perm/sign): Golf another proof

eric-wieser committed 5 years ago

ffbeb5f3

Newer Older