leanprover-community/mathlib

Pull Requests Commits

forgot to add module instance

dupuisf committed 4 years ago

ad993aa9

Merge branch 'dupuisf/semilinearize_bilinear_map' into dupuisf/semilinear_module_instance

dupuisf committed 4 years ago

6173349c

semilinearize bilinear maps

dupuisf committed 4 years ago

46ff5f54

done semilinearizing bilinear_map

dupuisf committed 4 years ago

80379ee1

trying to semilinearize operator_norm and bilinear_map

dupuisf committed 4 years ago

1f6e7bf0

dupuisf committed 4 years ago

6392b43d

dupuisf committed 4 years ago

185b2b7a

add module instance (still needs cleanup)

dupuisf committed 4 years ago

07710110

feat(order/lattice): add `inf_lt_sup` (#10178)

urkud committed 4 years ago

6cd6975d

feat(algebra/group/inj_surj): add `injective.monoid_pow` etc (#10152)

urkud committed 4 years ago

85f64207

feat(category_theory/limits/shapes/multiequalizer): Multi(co)equalizers (#10169)

adamtopaz committed 4 years ago

d69501f1

chore(*complex*): add a few simp lemmas (#10187)

urkud committed 4 years ago

cc59673b

feat(analysis/calculus/times_cont_diff): `equiv.prod_assoc` is smooth. (#10165)

ocfnash committed 4 years ago

a71bfdca

refactor(data/multiset/locally_finite): Generalize `multiset.Ico` to locally finite orders (#10031)

YaelDillies committed 4 years ago

d9a80ee9

feat(combinatorics/simple_graph): adding simple_graph.support and mem_support / support_mono lemmas (#10176)

arthurpaulino committed 4 years ago

5f5ce2b4

chore(linear_algebra/affine_space/affine_map): make `affine_map.coe_sub` true by definition (#10182)

ocfnash committed 4 years ago

8ac2fa06

refactor(measure_theory/integral/bochner): remove superfluous hypothesis (#10181)

fpvandoorn committed 4 years ago

b22a7c7e

feat(algebra/order/with_zero): add with_zero.linear_ordered_comm_grou… (#10180)

mariainesdff committed 4 years ago

88b4ce73

refactor(algebra/group): move `monoid.has_pow` etc to `algebra.group.defs` (#10147)

urkud committed 4 years ago

b31af6d9

feat(data/quot): add `quotient.lift₂_mk` (#10173)

shingtaklam1324 committed 4 years ago

16af388f

chore(data/bool): add `bool.lt_iff` (#10179)

urkud committed 4 years ago

35d36288

feat(measure_theory/covering/vitali_family): define Vitali families (#10057)

sgouezel committed 4 years ago

8991f28d

doc(group_theory/sylow): Expand Frattini's argument docstring (#10174)

tb65536 committed 4 years ago

6f9ec121

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

leanprover-community-bot committed 4 years ago

8490f2aa

feat(number_theory/lucas_primality): Add theorem for Lucas primality test (#8820)

BoltonBailey committed 4 years ago

41a820dd

feat(data/finset/prod): When `finset.product` is nonempty (#10170)

YaelDillies committed 4 years ago

d6a57f89

feat(data/fin/interval): Cardinality of `finset.Ixi`/`finset.Iix` in `fin` (#10168)

YaelDillies committed 4 years ago

b064622f

chore(topology/continuous_function/bounded): add simple lemmas (#10149)

urkud committed 4 years ago

fab61c9f

feat(algebra/group_with_zero/basic): relax some commutativity assumptions (#10075)

alexjbest committed 4 years ago

466fd276

feat(data/equiv/mul_add): add lemmas about multiplication and addition on a group being bijective and finite cancel_monoid_with_zeros (#10046)

alexjbest committed 4 years ago

ce0e0583

Older