leanprover-community/mathlib3

Pull Requests Commits

erdOne committed 4 years ago

c79e4cd6

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

refactor(algebra/floor): Rename floor and ceil functions (#9590)

YaelDillies committed 4 years ago

9da33a89

refactor(analysis/special_functions): generalise nth-root lemmas (#9704)

jchoules committed 4 years ago

264ff903

chore(category_theory/sites/*): Generalize universes (#9675)

adamtopaz committed 4 years ago

8d67d9ae

chore(set_theory/cardinal): rename `is_empty`/`nonempty` lemmas (#9668)

urkud committed 4 years ago

34f34942

feat(algebra/bounds): `smul` of upper/lower bounds (#9078)

YaelDillies committed 4 years ago

33406172

feat(combinatorics/hall): generalized Hall's Marriage Theorem (#7825)

kmill committed 4 years ago

19da20b0

feat(set_theory/cardinal): add lemmas (#9697)

riccardobrasca committed 4 years ago

5db83f9c

chore(data/real/irrational): add more lemmas (#9684)

urkud committed 4 years ago

3faf0f5d

feat(topology/connected.lean): add theorems about connectedness o… (#9633)

AntoineChambert-Loir committed 4 years ago

096923c0

chore(ring_theory/ideal): improve 1st isomorphism theorem docstrings (#9699)

Vierkantor committed 4 years ago

32e1b6c1

refactor(algebra/group_power/order): relax linearity condition on `one_lt_pow` (#9696)

YaelDillies committed 4 years ago

0ce44420

refactor(linear_algebra/dimension): remove some nontrivial assumptions (#9693)

riccardobrasca committed 4 years ago

bc9e38f4

feat(measure_theory/covering/besicovitch): remove measurability assumptions (#9679)

sgouezel committed 4 years ago

313db47a

refactor(data/set/pairwise): generalize `pairwise_disjoint` to `semilattice_inf_bot` (#9670)

YaelDillies committed 4 years ago

f29755b9

Older