leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into YK-finite-set

urkud committed 3 years ago

18c98c18

chore(algebra/associated): make `irreducible` not a class (#14713)

ericrbg committed 3 years ago

2d76f563

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

leanprover-community-bot committed 3 years ago

855ed5c1

chore(group_theory/group_action/opposite): add a missed smul/scalar rename (#15082)

eric-wieser committed 3 years ago

56544106

feat(data/fintype/basic): add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. (#15080)

linesthatinterlace committed 3 years ago

774e6803

chore(group_theory/group_action/basic): relax monoid to mul_one_class (#15051)

eric-wieser committed 3 years ago

9fcf391e

feat(topology/uniform_space/basic): uniform continuity from/to an infimum of uniform spaces (#14892)

ADedecker committed 3 years ago

e94e5c08

feat(order/lattice, data/set): some helper lemmas (#14789)

apnelson1 committed 3 years ago

ff5e97ad

feat(linear_algebra/*): add lemma `linear_independent.finite_of_is_noetherian` (#14714)

ocfnash committed 3 years ago

7f95e220

chore(data/set,topology): fix 2 lemma names (#15079)

urkud committed 3 years ago

2ae20651

feat(ring_theory): Some missing lemmas (#15064)

erdOne committed 3 years ago

8b69a4b2

feat(topology/separation): `separation_quotient α` is a T₀ space (#15043)

urkud committed 3 years ago

36ee9aff

feat(order/locally_finite): make `fintype.to_locally_finite_order` computable (#14733)

eric-wieser committed 3 years ago

0369f202

refactor(ring_theory/jacobson): remove unnecessary `fintype.trunc_equiv_fin` (#15077)

kmill committed 3 years ago

0522ee08

refactor(ring_theory/finiteness): remove unnecessary `fintype.trunc_equiv_fin` (#15076)

kmill committed 3 years ago

640955c6

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

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

eric-wieser committed 3 years ago

ce332c11

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

Older