leanprover-community/mathlib

Pull Requests Commits

feat(data/nat/enat): simple lemmas on `enat` (#15029)

vihdzp committed 3 years ago

f9b939c3

chore(algebra/order/monoid): golf proofs, fix docs (#14728)

urkud committed 3 years ago

6e362f68

feat(data/list/basic): add filter_map_join (#14777)

madvorak committed 3 years ago

9e97baae

feat (analysis/normed_space/lp_space):add l_infinity ring instances (#14104)

CameronTorrance committed 3 years ago

e73ac940

streamline tests

adomani committed 3 years ago

334510ae

adomani committed 3 years ago

5143e529

refactor(algebra/group_power): split ring lemmas into a separate file (#15032)

eric-wieser committed 3 years ago

ce332c11

extra test for failure

adomani committed 3 years ago

663437ee

adomani committed 3 years ago

a8a7f6ad

adomani committed 3 years ago

1f83d2c9

Merge branch 'master' into adomani_compute_degree_le

adomani committed 3 years ago

6ffa89bf

Merge branch 'master' into adomani_compute_degree_le

adomani committed 3 years ago

e4623250

adomani committed 3 years ago

0849a1d6

adomani committed 3 years ago

e9631d37

feat(algebra/category/Module): upgrade `free : Type ⥤ Module R` to a monoidal functor (#14328)

kim-em committed 3 years ago

7e244d8b

chore(data/nat/factorization/basic): delete `import tactic.linarith` (#15075)

stuart-presnell committed 3 years ago

9229b0e0

feat(data/fin/basic): `induction_zero` and `induction_succ` lemmas (#15060)

technosentience committed 3 years ago

e7425e7b

refactor(algebra/group/defs): rename has_scalar to has_smul (#14559)

berndlosert committed 3 years ago

806bbb01

refactor(algebra/hom/group): generalize basic API of `monoid_hom` to `monoid_hom_class` (#14997)

dupuisf committed 3 years ago

c10efa66

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

Newer Older