leanprover-community/mathlib3

Pull Requests Commits

refactor(analysis/normed_space/hahn_banach): use is_R_or_C instead of specific typeclass (#5009)

sgouezel committed 5 years ago

17a6f6da

chore(algebra/ordered_group): move monoid stuff to ordered_monoid.lean (#5066)

kbuzzard committed 5 years ago

2a876b65

chore(data/fin): a few more lemmas about `fin.insert_nth` (#5079)

urkud committed 5 years ago

8d71ec99

chore(topology/metric_space/isometry): add a missing simp lemma (#5078)

urkud committed 5 years ago

c4587245

chore(algebra/big_operators): add `finset.abs_prod` (#5076)

urkud committed 5 years ago

a9b6b362

chore(measure_theory/borel_space): add some `simp` attrs (#5075)

urkud committed 5 years ago

2ba930eb

chore(topology/basic): add `cluster_pt.map`, rename `mem_closure` (#5065)

urkud committed 5 years ago

c59dbf3d

chore(analysis/complex/basic): add `times_cont_diff.real_of_complex` (#5073)

urkud committed 5 years ago

a6498516

chore(logic/basic): add `forall_apply_eq_imp_iff₂` (#5072)

urkud committed 5 years ago

87439b98

chore(topology/homeomorph): add more simp lemmas (#5069)

urkud committed 5 years ago

198f3e54

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

leanprover-community-bot committed 5 years ago

8525aa98

feat(data/complex/is_R_or_C): Create a proper coercion from ℝ (#4824)

dupuisf committed 5 years ago

79cd7204

feat(data/nat/parity): lemmas about (-1)^n (#5056)

kbuzzard committed 5 years ago

556a7255

feat(group_theory/subgroup): add closure_eq_bot_iff (#5055)

kbuzzard committed 5 years ago

aff4669b

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

leanprover-community-bot committed 5 years ago

cff497f8

feat(algebra/group_power/basic): add add le_of_pow_le_pow (#5054)

kbuzzard committed 5 years ago

006f84ec

fix(linear_algebra/quadratic_form): nondegenerate -> anisotropic (#5050)

jcommelin committed 5 years ago

1fbdf771

feat(measure_theory/lp_space): prove that neg and add are in Lp (#5014)

RemyDegenne committed 5 years ago

498d4977

feat(linear_algebra/quadratic_form): nondegenerate quadratic forms (#5045)

eric-wieser committed 5 years ago

32d1dfcb

feat(analysis/special_functions/pow): add ennreal.to_nnreal_rpow (#5042)

RemyDegenne committed 5 years ago

8d40e8d0

feat(number_theory/arithmetic_function): moebius is the inverse of zeta (#5001)

awainverse committed 5 years ago

de76acdc

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

leanprover-community-bot committed 5 years ago

0e976d95

feat(ring_theory/witt_vector/verschiebung): verschiebung of witt vectors (#4836)

jcommelin committed 5 years ago

47542a04

chore(field_theory/minimal_polynomial): generalize irreducible (#5006)

riccardobrasca committed 5 years ago

33265106

feat(algebra/*): star_ring instances on free_algebra, free_monoid, ring_quot, and quaternion (#4902)

kim-em committed 5 years ago

b479d3bb

chore(algebra/group/defs): Remove shortcut instance definitions (#4955)

eric-wieser committed 5 years ago

700d5761

feat(category_theory/limits): terminal comparison morphism (#5025)

b-mehta committed 5 years ago

123c5221

feat(algebra/squarefree): a squarefree element of a UFM divides a power iff it divides (#5037)

awainverse committed 5 years ago

b848b5b5

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

leanprover-community-bot committed 5 years ago

87a6d95b

chore(field_theory/separable): spell-check "seperable" to "separable" (#5040)

awainverse committed 5 years ago

68adaba3

Newer Older