leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/special_functions/trigonometric): Added lemma cos_ne_zero_iff (#3743)

benjamindavidson committed 5 years ago

b1e56a21

chore(data/finset/order): use `[nonempty]` in `directed.finset_le` (#3759)

urkud committed 5 years ago

ced74696

chore(data/fintype/card): add `prod_bool` (#3758)

urkud committed 5 years ago

4c24a091

chore(data/fintype/card): DRY using `@... (multiplicative _)` (#3756)

urkud committed 5 years ago

31a0258b

feat(analysis/calculus/fderiv): multiplication by a complex respects real differentiability (#3731)

sgouezel committed 5 years ago

cc6528e7

feat(data/list/palindrome): define palindromes (#3729)

lambda-fairy committed 5 years ago

cfcbea6e

feat(algebra/order): more lemmas for projection notation (#3753)

fpvandoorn committed 5 years ago

c503b7af

fix(algebra/field) remove `one_div_eq_inv` (#3749)

fpvandoorn committed 5 years ago

6c8b2cd6

feat(tactic/clear_value): preserve order and naming (#3700)

cipher1024 committed 5 years ago

d6ffc1ad

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

leanprover-community-bot committed 5 years ago

cacb54ec

feat(tactic/choose): `choose` can now decompose conjunctions (#3699)

cipher1024 committed 5 years ago

486830b0

feat(tactic/rcases): type ascriptions in rcases (#3730)

digama0 committed 5 years ago

f8c81351

feat(.): add code of conduct (#3747)

robertylewis committed 5 years ago

4324778f

feat(field_theory/algebraic_closure): algebraic closure (#3733)

kckennylau committed 5 years ago

eb4b2a05

feat(topology/opens): open_embedding_of_le (#3597)

kim-em committed 5 years ago

bfcf6400

docs(category/default): Fix typo for monomorphism (#3741)

utensil committed 5 years ago

06e14052

refactor(algebra/divisibility, associated): generalize instances in divisibility, associated (#3714)

awainverse committed 5 years ago

f92fd0d1

feat(haar_measure): define the Haar measure (#3542)

fpvandoorn committed 5 years ago

57df7f5a

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

leanprover-community-bot committed 5 years ago

43ceb3e0

chore(algebra/ordered_field): cleanup (#3723)

urkud committed 5 years ago

9e039956

feat(group_theory/group_action): generalize `is_algebra_tower` (#3717)

Vierkantor committed 5 years ago

4a75df92

feat(tactic): fix two bugs with generalize' (#3710)

fpvandoorn committed 5 years ago

37e97b53

feat(category_theory/limits): explicit isomorphisms between preserved limits (#3602)

kim-em committed 5 years ago

47861363

chore(category_theory/limits): minor changes in equalizers and products (#3603)

kim-em committed 5 years ago

5680428f

refactor(linear_algebra/affine_space): split up file (#3726)

jsm28 committed 5 years ago

17ef529d

doc(tactic/lean_core_docs): by_cases is classical (#3718)

lambda-fairy committed 5 years ago

f23fe9a3

chore(linear_algebra/basic): rewrite `p.comap q.subtype` to `comap q.subtype p` (#3725)

Vierkantor committed 5 years ago

d27ddb49

chore(order/complete_lattice): use `order_dual` (#3724)

urkud committed 5 years ago

1675dc40

feat(linear_algebra/finite_dimensional): finite dimensional `is_basis` helpers (#3720)

Vierkantor committed 5 years ago

bf1c7b75

feat(algebra/classical_lie_algebras): add lie_algebra.orthogonal.mem_so (#3711)

Oliver Nash committed 5 years ago

d61bd4ae

Newer Older