leanprover-community/mathlib

Pull Requests Commits

feat(data/nat/prime): prime.even_iff (#14688)

BoltonBailey committed 3 years ago

6b4f3f2b

refactor(src/algebra/order/monoid): make bot_eq_zero a simp lemma only when the order is linear (#14553)

eric-wieser committed 3 years ago

e86ab0b0

feat(number_theory/cyclotomic/primitive_roots): generalize finrank lemma (#14550)

riccardobrasca committed 3 years ago

b4b816c9

chore(field_theory/intermediate_field): fix timeout (#14725)

alreadydone committed 3 years ago

38ad656e

feat(logic/hydra): basic lemmas on `cut_expand` (#14408)

vihdzp committed 3 years ago

dd4d8e6a

feat(set_theory/game/basic): cast inequalities on `pgame` to `game` (#14405)

vihdzp committed 3 years ago

a16f1cfe

feat(data/vector/basic): reflected instance for vectors (#14669)

eric-wieser committed 3 years ago

bf2edb5d

refactor(set_theory/game/state): rename `pgame.of` to `pgame.of_state` (#14658)

vihdzp committed 3 years ago

b134b2f5

feat(set_theory/cardinal/basic): improve docs on `lift`, add `simp` lemmas (#14596)

vihdzp committed 3 years ago

7b2970fa

feat(data/nat/factorization): add lemma `coprime_of_div_pow_factorization` (#14576)

stuart-presnell committed 3 years ago

2e2d5155

feat(topology/homotopy/contractible): a few convenience lemmas (#14710)

urkud committed 3 years ago

16728b30

feat(analysis/special_functions/trigonometric/deriv): compare `sinh x` with `x` (#14702)

urkud committed 3 years ago

05aa9607

feat(order/monotone): add lemmas about `cmp` (#14689)

urkud committed 3 years ago

d5c72605

golf(set_theory/ordinal/basic): golf theorems on `cardinal.ord` and `ordinal.card` (#14709)

vihdzp committed 3 years ago

6cdc30d7

feat(linear_algebra/vandermonde): add lemmas about det equals zero (#14695)

bartmichels committed 3 years ago

ed033f39

feat({tactic + test}/congrm, logic/basic): `congrm = congr + pattern-match` (#14153)

adomani committed 3 years ago

41eb9587

feat(topology/homeomorph): add `homeomorph.set.univ` (#14730)

urkud committed 3 years ago

32d8fc4e

feat(analysis/special_functions/exp): add `real.exp_half` (#14729)

urkud committed 3 years ago

1c8f995c

feat(data/complex/basic): ranges of `re`, `im`, `norm_sq`, and `abs` (#14727)

urkud committed 3 years ago

da5a737b

refactor(algebra/order/group): unify instances (#14705)

urkud committed 3 years ago

b11f8e7f

feat(algebra/algebra/basic): define `alg_hom_class` and `non_unital_alg_hom_class` (#14679)

dupuisf committed 3 years ago

2b469927

feat(order/{conditionally_complete_lattice,galois_connection): Supremum of `set.image2` (#14307)

YaelDillies committed 3 years ago

5d18a722

feat(algebra/lie/weights): the zero root space is the Cartan subalgebra for a Noetherian Lie algebra (#14174)

ocfnash committed 3 years ago

300c4395

feat(set_theory/cardinal/cofinality): lemma on subsets of strong limit cardinal (#14442)

vihdzp committed 3 years ago

67dfb57c

fix(data/list/nodup): change `Type` to `Type u` (#14721)

user7230724 committed 3 years ago

7fee0f12

feat(logic/equiv/basic): add `Pi_comm` aka `function.swap` as an `equiv` (#14561)

ADedecker committed 3 years ago

659983c6

refactor(algebra/order/monoid): Split field of `canonically_ordered_...` (#14556)

YaelDillies committed 3 years ago

18bf7af3

refactor(data/option/defs): Swap arguments to `option.elim` (#14681)

YaelDillies committed 3 years ago

2967fae8

feat(set_theory/game/ordinal): golf `to_pgame_birthday` (#14662)

vihdzp committed 3 years ago

425dfe76

doc(ring_theory/algebraic): clarify docstring (#14715)

kbuzzard committed 3 years ago

3afafe6b

Newer Older