leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 5 years ago

7444c0d0

refactor(data/bundled_set): Add an is_bundled_set predicate to deduplicate bundled object coercions

eric-wieser committed 5 years ago

42045ce6

fix(data/dfinsupp): fix overly strict type-class arguments (#5935)

eric-wieser committed 5 years ago

c43c709f

feat(analysis/normed_space/inner_product): existence of orthonormal basis (#5734)

hrmacbeth committed 5 years ago

82481e30

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

leanprover-community-bot committed 5 years ago

95454452

feat(archive/imo): formalize IMO 2013 problem Q5 (#5787)

dwrensha committed 5 years ago

6585eff9

feat(ring_theory/nullstellensatz): Classical Nullstellensatz (#5760)

dtumad committed 5 years ago

3e599600

refactor(data/set/basic): simpler proofs (#5920)

digama0 committed 5 years ago

4cc0d525

feat(data/fintype/basic): make subtype_of_fintype computable (#5919)

pechersky committed 5 years ago

8af7e08e

feat(algebra/*,linear_algebra/basic,ring_theory/ideal): lemmas about span of finite subsets and nontrivial maximal ideals (#5641)

Vierkantor committed 5 years ago

f45dee43

feat(data/zsqrtd/to_real): Add `to_real` (#5640)

eric-wieser committed 5 years ago

32fdb81b

feat(algebra/continued_fractions): add termination iff rat lemmas (#4867)

kappelmann committed 5 years ago

1011601d

feat(order/ideal): add partial_order instance to order.ideal (#5909)

mguaypaq committed 5 years ago

9adf9bb6

refactor(topology/local_homeomorph): simpler proof of `prod_symm` (#5906)

Jesse Michael Han committed 5 years ago

7244b43c

refactor(computability/primrec): simpler proof of `primrec.of_equiv` (#5905)

Jesse Michael Han committed 5 years ago

a859f10d

refactor(data/set/basic): simpler proof of `union_subset_iff` (#5904)

Jesse Michael Han committed 5 years ago

35638edb

chore(*): bump to lean-3.26.0 (#5895)

jcommelin committed 5 years ago

c64aa132

feat(measure_theory/independence): define independence of sets of sets, measurable spaces, sets, functions (#5848)

RemyDegenne committed 5 years ago

78a518a3

refactor(category_theory/abelian): golf `mono_of_kernel_ι_eq_zero` (#5914)

Jesse Michael Han committed 5 years ago

e5f9409c

refactor(data/complex/exponential): simplify proof of `tan_eq_sin_div_cos` (#5913)

Jesse Michael Han committed 5 years ago

1688b3e8

refactor(data/holor): simp -> refl (#5912)

Jesse Michael Han committed 5 years ago

e927930c

refactor(algebra/category/Group/limits): simp -> refl (#5911)

Jesse Michael Han committed 5 years ago

38f6e050

refactor(data/real/golden_ratio): simpler proof of `gold_pos` (#5910)

Jesse Michael Han committed 5 years ago

6eae6303

refactor(data/pequiv): simpler proof of `pequiv.of_set_univ` (#5907)

Jesse Michael Han committed 5 years ago

e9a1e2b3

refactor(algebra/group/basic): simp -> rw in `sub_eq_sub_iff_sub_eq_sub` (#5903)

Jesse Michael Han committed 5 years ago

fd55e57f

chore(data/finset/preimage): add missing simp lemmas (#5902)

eric-wieser committed 5 years ago

1cd22862

chore(*): add more simp lemmas, refactor theorems about `fintype.sum` (#5888)

urkud committed 5 years ago

20d6b6a7

feat(algebra/euclidean_domain): Unify occurences of div_add_mod and mod_add_div (#5884)

Julian-Kuelshammer committed 5 years ago

21e9d424

refactor(ring_theory/ideal ring_theory/jacobson): allow `ideal` in a `comm_semiring` (#5879)

adomani committed 5 years ago

688772e9

feat(ring_theory/noetherian, linear_algebra/basic): Show that finitely generated submodules are the compact elements in the submodule lattice (#5871)

cemulate committed 5 years ago

b2c5d9b2

Older