leanprover-community/mathlib3

Pull Requests Commits

chore(algebra/order/monoid): move lemmas (#16176)

urkud committed 3 years ago

cf7b16a6

feat(data/rat/cast): drop an unneeded typeclass assumption (#15972)

urkud committed 3 years ago

6a5a2b13

feat(data/sym/basic): add nil coe lemma (#16181)

pimotte committed 3 years ago

07052296

feat(algebra/order/ring): generalize some `mono` lemmas, use them (#14691)

urkud committed 3 years ago

bfd28571

feat(*): rsuffices golfs (#16159)

ericrbg committed 3 years ago

6155d435

refactor(analysis/convex/basic): Redefine convexity in terms of star-convexity (#16173)

YaelDillies committed 3 years ago

0da54467

chore(analysis/inner_product_space): move `is_symmetric` to a new file lower in the import tree (#16106)

ADedecker committed 3 years ago

90bc9579

feat(data/set/prod): decidable mem instance on set prod (#16107)

dtumad committed 3 years ago

175a0959

feat(algebra/*): Algebraic instances on `lex`/`order_dual` (#16122)

YaelDillies committed 3 years ago

e0b2fa6d

refactor(data/int/cast): Use hom classes (#16024)

YaelDillies committed 3 years ago

972aa423

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

leanprover-community-bot committed 3 years ago

b46c8953

chore(algebra/big_operators/pi): rename `w` to `H` in assumptions (#16166)

urkud committed 3 years ago

ec73f6e3

feat(group_theory/coset): Right cosets are orbits (#16119)

tb65536 committed 3 years ago

aac3141e

feat(set_theory/cardinal/finite): `nat.card (zmod n) = n` (#16118)

tb65536 committed 3 years ago

eaeb4583

feat(algebraic_topology): split simplicial objects (#16072)

joelriou committed 3 years ago

df967907

feat(algebra/order/complete_field): generalize ring_hom_monotone (#16147)

alreadydone committed 3 years ago

ee261437

refactor(order/minimals): Change definition to `a ≤ b → b ≤ a` (#16103)

YaelDillies committed 3 years ago

67488dff

chore(field_theory/*): Fix lint (#16149)

YaelDillies committed 3 years ago

c2c31b52

feat(data/finset/pointwise): `-s • t = -(s • t)` (#16138)

YaelDillies committed 3 years ago

4a0f332e

split(analysis/convex/segment): Split off `analysis/convex.basic` (#16112)

YaelDillies committed 3 years ago

4705dd0d

feat(ring_theory/polynomial): Vieta's formula in terms of `polynomial.roots` (#14908)

alreadydone committed 3 years ago

8fdec909

feat(algebra/star/star_alg_hom): define unital and non-unital `star_alg_hom`s (#16089)

j-loreaux committed 3 years ago

09d7fe37

chore(data/finsupp/ne_locus): reduce import, after the finsupp.basic refactor (#16165)

adomani committed 3 years ago

2c6e5959

feat(order/complete_lattice): Duals of complete lattice operations (#16148)

YaelDillies committed 3 years ago

21b64128

fix(control/random): typo (#16156)

oxarbitrage committed 3 years ago

e1b7b7d5

chore(linear_algebra/matrix/block): remove the `_matrix` suffix from `matrix.block_triangular_matrix` (#16155)

eric-wieser committed 3 years ago

e8ca35f1

feat(algebra/group_with_zero): slightly generalise mul_ne_zero (#16137)

ericrbg committed 3 years ago

faed3a7f

feat(ring_theory/valuation/valuation_subring): pointwise left actions via `map` (#16080)

eric-wieser committed 3 years ago

e57e72fd

feat(data/finsupp/ne_locus): new file with finsupp.ne_locus (#16091)

adomani committed 3 years ago

5ad44a90

refactor(data/finsupp/basic): split `data/finsupp/basic` into three parts (#15699)

stuart-presnell committed 3 years ago

f9c30004

Newer Older