leanprover-community/mathlib

Pull Requests Commits

make reals computable

gebner committed 4 years ago

ced6285c

Fix proof in specific_limits

gebner committed 4 years ago

1a604b60

New approach for making ℝ irreducible.

gebner committed 4 years ago

4bf7fb85

refactor(data/real/basic): make real a structure

gebner committed 4 years ago

f8dadb5c

doc(algebra/{archimedean, char_zero}): provide docstrings (#6010)

Julian-Kuelshammer committed 4 years ago

e1ca806c

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

leanprover-community-bot committed 4 years ago

e66ad5f5

feat(order/compactly_generated): Show that the sublattice below a compact element is coatomic (#5942)

cemulate committed 4 years ago

79ca6e23

feat(algebra/ring): add mk_mul_self_of_two_ne_zero (#5862)

alexjbest committed 4 years ago

fcad25f2

feat(data/fintype/sort): add `fin_sum_equiv_of_finset` (#6008)

urkud committed 4 years ago

2153dc34

refactor(measure_theory/*): rename `is_(null_)?measurable` to `(null_)?measurable_set` (#6001)

urkud committed 4 years ago

1b1ad15c

chore(analysis/normed_space/basic): use explicit arg `𝕜'` in lemmas about `normed_algebra` (#6009)

urkud committed 4 years ago

2b2edc97

fix(tactic/delta_instance): improve naming of instances with multiple arguments (#6007)

eric-wieser committed 4 years ago

4e786548

feat(geometry/manifold/instances): sphere is a smooth manifold (#5607)

hrmacbeth committed 4 years ago

fe9c021d

refactor(group_theory/perm): move perm.subtype_perm to basic (#6005)

pechersky committed 4 years ago

dbb5ca1e

feat(nat/basic): more nat.find lemmas (#6002)

fpvandoorn committed 4 years ago

9b3dc417

feat(analysis/normed_space/inner_product): remove unnecessary `nonneg_im` field (#5999)

gebner committed 4 years ago

6633a70e

feat(logic/function/basic): add bijective.iff_exists_unique and projections (#5995)

eric-wieser committed 4 years ago

508c2650

refactor(data/polynomial/eval): change eval_smul lemmas to use * instead of 2nd smul (#5991)

BoltonBailey committed 4 years ago

3732fb9d

feat(algebra/group_power/lemmas): sign of even/odd powers (#5990)

benjamindavidson committed 4 years ago

ff05d3af

refactor(linear_algebra,algebra/algebra): generalize `linear_map.smul_right` (#5967)

urkud committed 4 years ago

25c34e04

feat(data/nat/parity): addition/subtraction of even/odd nats (#5934)

benjamindavidson committed 4 years ago

fc7daa36

feat(tactic/norm_fin): tactic for normalizing `fin n` expressions (#5820)

pechersky committed 4 years ago

893ce8b6

refactor(*): rename subtype_congr to subtype_equiv (#6004)

pechersky committed 4 years ago

75a7ce9f

chore(topology/bases): rewrite 2 proofs using tactic mode (#5996)

urkud committed 4 years ago

fec8ee4e

feat(data/finset/basic): add lemmas about bUnion and images of functions on finsets (#5887)

agusakov committed 4 years ago

0c26bb09

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

leanprover-community-bot committed 4 years ago

2c62c0bd

feat(order/compactly_generated, ring_theory/noetherian): the lattice of submodules is compactly generated (#5944)

awainverse committed 4 years ago

a301ef7e

feat(combinatorics/simple_graph/basic): add decidable instance for adjacency of complement (#6000)

agusakov committed 4 years ago

4d3b26f8

feat(data/list/basic) add update_nth_comm (#5989)

alexjbest committed 4 years ago

1706e552

refactor(ring_theory/ideal/*, ring_theory/jacobson): use `comm_semiring` instead of `comm_ring` for ideals (#5954)

adomani committed 4 years ago

9b779f40

Older