leanprover-community/mathlib

Pull Requests Commits

Add import `data.nat.interval`

stuart-presnell committed 3 years ago

90a7db2d

stuart-presnell committed 3 years ago

962f3f21

Merge branch 'master' into SP_Legendre_factorization

stuart-presnell committed 3 years ago

92e36836

feat(topology/compact_open): continuous_comp left functor C(-, γ) (#15068)

ralvrz committed 3 years ago

eb852609

feat(number_theory/legendre_symbol/mul_character): alternative implementation (#14768)

MichaelStollBayreuth committed 3 years ago

050f9e6d

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

leanprover-community-bot committed 3 years ago

ad154bd0

feat(set_theory/cardinal/*): simp lemmas for `to_nat` and `to_enat` (#15059)

vihdzp committed 3 years ago

5d8810aa

feat(set_theory/game/pgame): golf `le_trans` (#14956)

vihdzp committed 3 years ago

68452ec1

feat(linear_algebra/linear_pmap): add has_smul and ext (#14915)

mcdoll committed 3 years ago

501c1d41

refactor(ring_theory/graded_algebra): use `add_submonoid_class` to generalize to graded rings (#14583)

eric-wieser committed 3 years ago

a2a8c9be

chore(set_theory/game/pgame): golf various theorems about relabellings (#15054)

vihdzp committed 3 years ago

1116684d

refactor(group_theory/coset): redefine quotient group to be quotient by action of subgroup (#15045)

hrmacbeth committed 3 years ago

108e3a07

feat(field_theory/minpoly): generalize statements about GCD domains (#14979)

riccardobrasca committed 3 years ago

71985dc5

feat(model_theory/satisfiability): The Łoś–Vaught Test (#14758)

fpvandoorn committed 3 years ago

6879dd0c

feat(algebra/order/monoid): `a + b ≤ c → a ≤ c` (#15033)

YaelDillies committed 3 years ago

397d45f2

chore(analysis/locally_convex/balanced_core_hull): Golf (#14987)

YaelDillies committed 3 years ago

07726e21

chore(data/nat/factorization/basic): golf rec_on_pos_prime_pos_coprime, remove import (#14935)

stuart-presnell committed 3 years ago

478773b8

refactor(logic/hydra): use `is_irrefl` (#15039)

vihdzp committed 3 years ago

ee8d588d

feat(tactic/alias.lean): use current namespace in alias (#14961)

digama0 committed 3 years ago

c8ab806e

feat(linear_algebra/linear_pmap): definition of the graph (#14920)

mcdoll committed 3 years ago

5de765c5

chore(group_theory/group_action/basic): split file (#15044)

hrmacbeth committed 3 years ago

aa812bd1

refactor(topology/*): Use `disjoint` (#14950)

YaelDillies committed 3 years ago

ea9dae21

feat(algebra/order/field): Linearly ordered semifields (#15027)

YaelDillies committed 3 years ago

03374ee3

feat(topology/algebra/module/basic): define continuous_(semi)linear_map_class (#14674)

dupuisf committed 3 years ago

55ec65a6

feat(order/succ_pred/basic): tag more lemmas with simp (#14998)

vihdzp committed 3 years ago

08b07a64

feat(order/boolean_algebra): Interaction of disjointness and complements (#14925)

YaelDillies committed 3 years ago

7db76670

feat(algebra/ring/boolean_ring): `bool` is a Boolean ring (#15004)

YaelDillies committed 3 years ago

00c17d65

feat(data/{finset, set}/basic): tweak `nonempty_coe_sort` and `is_empty_coe_sort` (#14937)

vihdzp committed 3 years ago

78bc3724

feat(probability_theory/independence): if a family of pi-systems is independent, then so are the generated measurable spaces (#9387)

RemyDegenne committed 3 years ago

3594b635

feat(measure_theory/function/lp_order): prove a `normed_lattice_add_comm_group` instance for Lp (#14999)

kex-y committed 3 years ago

728e074e

Older