leanprover-community/mathlib

Pull Requests Commits

remove unused instances

datokrat committed 3 years ago

026cb4f2

feat(linear_algebra/affine_space/affine_subspace): `affine_equiv.comap_span`

datokrat committed 3 years ago

531cfaca

fix(topology/fiber_bundle/basic): rename field of fiber_bundle_core (#17679)

fpvandoorn committed 3 years ago

8bab60f0

chore(geometry/manifold/mfderiv): make `model_with_corners` implicit in `has_mfderiv_at.add`, `has_mfderiv_at.mul` etc. (#17675)

CBirkbeck committed 3 years ago

98cdae56

feat(ring_theory/ideal): ideal norm evaluation lemmas (#17299)

Vierkantor committed 3 years ago

31c458dc

feat(analysis/calculus): smoothness of series of functions (#17110)

sgouezel committed 3 years ago

563bbc0c

feat(analysis/normed/group/add_circle): results about finite-order points on the circle (#17321)

ocfnash committed 3 years ago

084f76e2

chore(linear_algebra/linear_pmap): leq lemma (#17565)

mcdoll committed 3 years ago

8709a597

feat(data/finite/defs): add `ulift.infinite`/`plift.infinite` (#17655)

urkud committed 3 years ago

f69e8f31

feat(data/list/big_operators): add lemmas on products/sums (#17499)

MichaelStollBayreuth committed 3 years ago

cadea043

perf(analysis/complex/conformal): squeeze simps (#17667)

j-loreaux committed 3 years ago

3403c032

feat(order/modular_lattice): Modular lattices are lower modular (#17403)

MadPidgeon committed 3 years ago

124aa163

feat(tactic/print_sorry): add `#print_sorry_in` command (#16911)

fpvandoorn committed 3 years ago

3536f475

refactor(combinatorics/simple_graph/connectivity): fix simp lemmas for `to_delete_edges`, use dot notation for `transfer` lemmas (#17644)

kmill committed 3 years ago

99e8971d

chore(*): add mathlibport comments (#17642)

eric-wieser committed 3 years ago

4887d729

refactor(category_theory/limits/shapes/finite_products): review API, fix lint (#17623)

urkud committed 3 years ago

ac3ae212

chore(data/polynomial/basic): golf (#17656)

urkud committed 3 years ago

2a1e571f

chore(counterexamples/cyclotomic_105): golf (#17652)

urkud committed 3 years ago

72d7ae14

feat(topology/uniform_space/uniform_convergence): more locally uniform limit API (#17092)

vbeffara committed 3 years ago

18b61ef3

move(algebra/order/monoid/*): Relocate `zero_le_one_class` (#17646)

YaelDillies committed 3 years ago

4150728b

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

leanprover-community-bot committed 3 years ago

642c8c06

ci: run `add_port_comments.py` nightly (#17641)

eric-wieser committed 3 years ago

97f46ea9

feat(data/list/perm): add `list.perm.{join,join_congr}` (#17497)

eric-wieser committed 3 years ago

c9514469

feat(combinatorics/young): add equivalence between Young diagrams and lists of natural numbers (#17445)

jakelev committed 3 years ago

a22eb8a8

feat(group_theory/index): `nat.card` version of `card_dvd_of_le` (#17269)

tb65536 committed 3 years ago

404520a1

lint(*): fix `to_additive_doc` (#17624)

urkud committed 3 years ago

e88d7966

chore(*): add missing `coe_copy` and `copy_eq` (#17615)

urkud committed 3 years ago

9822b65b

feat(data/finset/basic): Map `finset.filter` under an `equiv` (#17513)

YaelDillies committed 3 years ago

6c17afb9

feat(group_theory/transfer): `¬ p ∣ card transfer_sylow.ker` (#17502)

tb65536 committed 3 years ago

0013cf77

lint(data/zmod/quotient): fix `fintype`/`finite` (#17613)

urkud committed 3 years ago

d8ac3380

Older