leanprover-community/mathlib

Pull Requests Commits

WIP: Fix usages of `equiv_fin`

Vierkantor committed 4 years ago

6b3be16b

chore(data/fintype): rework `fintype.equiv_fin` and dependencies

Vierkantor committed 4 years ago

2287b1c9

feat(data/option/basic): option valued choice operator (#7101)

kim-em committed 4 years ago

aa1fa0b2

feat(data/fintype): golf, move and dualise proof (#7126)

b-mehta committed 4 years ago

6610e8f5

chore(linear_algebra/multilinear): relax requirements on `multilinear_map.pi_ring_equiv` (#7117)

eric-wieser committed 4 years ago

991dc260

feat(test/integration): update with new examples (#7105)

benjamindavidson committed 4 years ago

0b52522e

feat(tactic/simps): allow composite projections (#7074)

fpvandoorn committed 4 years ago

6dd9a54c

feat(category_theory, algebra/category): AddCommGroup is well-powered (#7006)

TwoFX committed 4 years ago

29b834df

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

leanprover-community-bot committed 4 years ago

4e607eb0

feat(analysis/special_functions/integrals): integral of `cos x ^ 2 - sin x ^ 2` (#7012)

benjamindavidson committed 4 years ago

505ffa9c

feat(data/equiv/basic): swap_apply_eq_iff (#7102)

pechersky committed 4 years ago

92ec9493

chore(algebra/ring_quot): Provide `sub` explicitly to `ring_quot` (#7112)

eric-wieser committed 4 years ago

379dd7d5

chore(data/matrix/basic): add simp lemmas about `minor`, move `reindex` to `matrix.basic` since it knows nothing about linear algebra (#7083)

eric-wieser committed 4 years ago

54ac48ad

chore(data/set/finite): set.finite.sup (#7080)

pechersky committed 4 years ago

fb74f984

feat(data/fintype/basic): to_finset lattice lemmas (#7077)

pechersky committed 4 years ago

bcf5b1a6

feat(order/order_iso_nat): add another flavour of well-foundedness for partial orders (#5434)

Oliver Nash committed 4 years ago

56e52487

chore(category_theory/abelian): enable instances (#7106)

kim-em committed 4 years ago

f474756b

feat(topology/unit_interval): abstract out material about [0,1] (#7056)

kim-em committed 4 years ago

8e7028cd

feat(archive/imo): formalize IMO 2008 Q3 (#7025)

manuelcandales committed 4 years ago

c6b06369

refactor(analysis/normed_space/add_torsor): generalize to semi_normed_space (#7016)

riccardobrasca committed 4 years ago

9c2a3e7e

feat(group_theory/perm): define the permutation `(0 1 ... (i : fin n))` (#6815)

Vierkantor committed 4 years ago

c5ea4cdd

feat(group_theory/is_free_group): the property of being a free group (#7086)

dwarn committed 4 years ago

def96711

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

leanprover-community-bot committed 4 years ago

e8b217bf

fix(.github/PULL_REQUEST_TEMPLATE.md): Fix the gitpod button link, looks like it moved with an update (#7096)

alexjbest committed 4 years ago

b9d9bf0e

chore(*): fixup docs that don't parse/cause linting errors (#7088)

ericrbg committed 4 years ago

99c7d22e

chore(ring_theory/tensor_product): golf proofs (#7089)

jcommelin committed 4 years ago

c356c1f2

feat(measure_theory/group, measure_theory/bochner_integration): left translate of an integral (#6936)

benjamindavidson committed 4 years ago

f4214def

feat(topology/category/Profinite): Profinite_to_Top creates limits. (#7070)

adamtopaz committed 4 years ago

68bd3253

feat(algebra/big_operators/basic): edit `finset.sum/prod_range_succ` (#6676)

benjamindavidson committed 4 years ago

08aff2ca

feat(dynamics/fixed_points/basic): fixed_points_id simp lemma (#7078)

pechersky committed 4 years ago

d76b6493

Older