leanprover-community/mathlib

Pull Requests Commits

feat(data/int/succ_pred): `ℤ` is succ- and pred- archimedean (#9731)

YaelDillies committed 4 years ago

155f8e66

feat(data/finset/basic, lattice): Simple lemmas (#9723)

YaelDillies committed 4 years ago

e7440330

feat(analysis/normed/group/SemiNormedGroup/kernels): add explicit_cokernel.map (#9712)

riccardobrasca committed 4 years ago

bf34d9b8

feat(analysis/normed/group/SemiNormedGroup/kernels): add kernels (#9711)

riccardobrasca committed 4 years ago

686b3635

feat(analysis/normed/group/SemiNormedGroup): add iso_isometry_of_norm_noninc (#9710)

riccardobrasca committed 4 years ago

3d999265

feat(algebra/group_power/order): When a power is less than one (#9700)

YaelDillies committed 4 years ago

5ac586a6

feat(algebra/floor): Floor and ceil of `-a` (#9715)

YaelDillies committed 4 years ago

99b2d40e

feat(topology/metric_space/lipschitz): add `lipschitz_with.min` and `lipschitz_with.max` (#9744)

urkud committed 4 years ago

9ac2aa29

chore(topology/uniform_space/pi): add `uniform_continuous_pi` (#9743)

urkud committed 4 years ago

96ba8b6a

refactor(ring_theory/fractional_ideal): speedup a proof (#9738)

kim-em committed 4 years ago

e3622934

chore(topology/algebra/ordered): move some lemmas to a new file (#9745)

urkud committed 4 years ago

f40cd88c

feat(group_theory/subgroup/basic): Bottom subgroup has unique element (#9734)

tb65536 committed 4 years ago

150bbeab

feat(measure_theory/covering/vitali): Vitali covering theorems (#9680)

sgouezel committed 4 years ago

17665882

chore(data/list): move lemmas from data.list.basic that require algebra.group_power to a new file (#9728)

alexjbest committed 4 years ago

ea22ce39

refactor(algebra/gcd_monoid): remove superfluous old_structure_cmd (#9720)

kim-em committed 4 years ago

711aa755

feat(linear_algebra/linear_independent): add variant of `exists_linear_independent` (#9708)

ocfnash committed 4 years ago

b3f602b9

feat(linear_algebra/dimension): generalize dim_zero_iff_forall_zero (#9713)

riccardobrasca committed 4 years ago

d6fd5f5f

refactor(ring_theory/derivation): remove old_structure_cmd (#9724)

kim-em committed 4 years ago

ad6d4764

chore(data/set_like/basic): remove superfluous old_structure_cmd (#9722)

kim-em committed 4 years ago

a2737b4b

refactor(algebra/lie/basic): remove old_structure_cmd (#9721)

kim-em committed 4 years ago

6bc2a1a2

feat(tactic/by_contra): add by_contra' tactic (#9619)

jcommelin committed 4 years ago

77070364

chore(algebra/floor): general golf (#9716)

YaelDillies committed 4 years ago

be91f696

feat(order/succ_pred): `succ`-Archimedean orders (#9714)

YaelDillies committed 4 years ago

c37ea535

feat(algebra/star): star_linear_equiv (#9426)

eric-wieser committed 4 years ago

c12acedd

refactor(algebra/module/order): Make space argument explicit in the `order_iso` (#9706)

YaelDillies committed 4 years ago

158fbc5d

feat(linear_algebra/affine_space/affine_subspace): add lemma `affine_equiv.span_eq_top_iff` (#9695)

ocfnash committed 4 years ago

72789f57

feat(archive/abel_ruffini): speedup by squeezing (#9709)

alexjbest committed 4 years ago

cef78dd4

chore(analysis/p_series): add 2 more versions (#9703)

urkud committed 4 years ago

393fe700

feat(data/equiv/basic): prop_equiv_pempty (#9689)

kim-em committed 4 years ago

aff49a63

feat(data/equiv/basic): subtype_equiv_psigma (#9688)

kim-em committed 4 years ago

dc23dfa1

Newer Older