leanprover-community/mathlib3

Pull Requests Commits

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

feat(algebra/*): Add of_injective lemmas (#5034)

eric-wieser committed 5 years ago

dcbec39a

feat(analysis/special_functions/pow): prove measurability of rpow for ennreal (#5026)

RemyDegenne committed 5 years ago

2de8db42

refactor(*): make continuous a structure (#5035)

sgouezel committed 5 years ago

abb0b678

feat(algebra/free_algebra): Add a nontrivial instance (#5033)

eric-wieser committed 5 years ago

38d2b53a

feat(category_theory/is_connected): zigzag lemmas (#5024)

b-mehta committed 5 years ago

0e09ada8

chore(data/complex/is_R_or_C): Remove two unnecessary axioms (#5017)

eric-wieser committed 5 years ago

aff77270

doc(algebra/module/linear_map): Explain where the ring instance is (#5023)

eric-wieser committed 5 years ago

d22a878e

feat(category_theory): constant functor is faithful (#5022)

b-mehta committed 5 years ago

dfdad99f

feat(category_theory/is_connected): transfer across equivalence (#5021)

b-mehta committed 5 years ago

dab2ae38

Newer Older