leanprover-community/mathlib

Pull Requests Commits

erdOne committed 3 years ago

8aa5aae3

generalize stuff

erdOne committed 3 years ago

25aab4c3

erdOne committed 3 years ago

943bf1dc

erdOne committed 3 years ago

8ec38b19

erdOne committed 3 years ago

1c6d66e0

Merge branch 'bijective_local' of https://github.com/leanprover-community/mathlib into bijective_local

erdOne committed 3 years ago

5425ad39

Update src/ring_theory/local_properties.lean

erdOne committed 3 years ago

Verified 9376ba1e

Update local_properties.lean

erdOne committed 3 years ago

Verified 2f3cb777

Update local_properties.lean

erdOne committed 3 years ago

Verified 7a481e33

erdOne committed 3 years ago

f9d2a546

erdOne committed 3 years ago

846d4a24

erdOne committed 3 years ago

462ad3fc

feat(analysis/normed_space/spectrum): lemmas about spectral radius, spectral mapping and `alg_hom_class` maps into the base field (#17178)

j-loreaux committed 3 years ago

ef61778b

feat(data/pfun): review APIs, add some lemmas about `fix_induction` (#17004)

astrainfinita committed 3 years ago

13bc7a20

chore(data/fintype/basic): don't reimplement finset.map (#17460)

eric-wieser committed 3 years ago

52d7570d

feat(data/nat/gcd/basic): add `nat.dvd_mul` and `dvd_mul` (#17131)

eric-wieser committed 3 years ago

b7a54188

chore(data/finsupp/defs): redefine `finsupp.single` as `pi.single` (#17356)

eric-wieser committed 3 years ago

d61f638a

feat(number_theory/divisors): more thoroughly link `divisors_antidiagonal` and `divisors` (#17050)

eric-wieser committed 3 years ago

c66f2aee

feat(algebra/*): add coercions from hom classes to their respective homs (#17000)

j-loreaux committed 3 years ago

dfd46033

chore(topology/fiber_bundle): move trivializations to a new file (#17463)

hrmacbeth committed 3 years ago

0b00e53a

feat(topology/algebra/const_mul_action): support of a function composed with smul (#17456)

sgouezel committed 3 years ago

18b38810

feat(tactic/move_add, test/move_add): a tactic for moving around summands (#13483)

adomani committed 3 years ago

e8b1a293

feat(analysis/convolution): weaken typeclass assumptions (#17452)

sgouezel committed 3 years ago

262dfc94

Revert "fix timeouts"

kim-em committed 3 years ago

23cd34bb

kim-em committed 3 years ago

933620c0

feat(topology/metric_space/basic): a continuous function is bounded on a neighborhood of a compact set (#17457)

sgouezel committed 3 years ago

08a8fd81

feat(geometry/euclidean/angle/oriented/affine): midpoint lemmas (#17444)

jsm28 committed 3 years ago

75351039

feat(analysis/[seminorm, locally_convex/with_seminorms]): semilinearize `seminorm.comp` (#17286)

ADedecker committed 3 years ago

a990661d

feat(analysis/normed_space/basic): the left-regular representation is an isometry for (even non-unital) C⋆-algebras (#16964)

j-loreaux committed 3 years ago

b75fd415

feat(topology/uniform_space): ulift as a uniform equiv (#17451)

sgouezel committed 3 years ago

1499a80b

Older