leanprover-community/mathlib

Pull Requests Commits

feat(linear_algebra/multilinear/basis): multilinear maps on basis vectors (#10090)

jsm28 committed 4 years ago

ef68f556

chore(ring_theory/noetherian): golf and generalize map_fg_of_fg (#10217)

eric-wieser committed 4 years ago

eb678347

feat(algebra/direct_sum): specialize `submodule_is_internal.independent` to add_subgroup (#10108)

eric-wieser committed 4 years ago

5ba41d8f

chore(ring_theory/ideal/operations): relax the base ring of algebras from comm_ring to comm_semiring (#10024)

eric-wieser committed 4 years ago

0dabcb8e

feat(data/finset/basic): add card_insert_eq_ite (#10209)

BoltonBailey committed 4 years ago

b4a5b013

chore(algebra/algebra/basic): add `algebra.coe_linear_map` (#10204)

eric-wieser committed 4 years ago

2fd6a77c

feat(analysis/{seminorm, convex/specific_functions}): A seminorm is convex (#10203)

YaelDillies committed 4 years ago

4dd7ecae

feat(linear_algebra/basic): some lemmas about span and restrict_scalars (#10167)

eric-wieser committed 4 years ago

e44aa6e7

feat(measure_theory/measure/complex): define complex measures (#10166)

kex-y committed 4 years ago

fb0cfbd4

feat(analysis/convex/combination): Convex hull of a `set.prod` and `set.pi` (#10125)

YaelDillies committed 4 years ago

e4a1e80f

feat(analysis): lemmas about `arg` and `exp_map_circle` (#10066)

urkud committed 4 years ago

1fac00e8

feat(analysis/special_functions/complex/arg): continuity of arg outside of the negative real half-line (#9500)

RemyDegenne committed 4 years ago

48abaedc

split(data/list/*): split off `data.list.basic` (#10164)

YaelDillies committed 4 years ago

32c8445a

chore(algebra/direct_sum/module): extract out common `variables` (#10207)

hrmacbeth committed 4 years ago

380d6cae

feat(algebra/order/with_zero): add le lemmas (#10183)

mariainesdff committed 4 years ago

bf242b78

refactor(linear_algebra/matrix/nonsingular_inverse): clean up (#10175)

eric-wieser committed 4 years ago

e0aa9f07

feat(archive/imo) : Add solution to IMO 1994 Q1 (#10171)

antoinelab01 committed 4 years ago

bc55cd78

feat(measure_theory/measurable_space): define `measurable_embedding` (#10023)

urkud committed 4 years ago

62f94ad6

docs(algebra/big_operators): correct documentation for prod (#10206)

EPronovost committed 4 years ago

c50c2c32

chore(measure_theory/measure): review API of `mutually_singular` (#10186)

urkud committed 4 years ago

ae98aad6

refactor(measure_theory/function/l1_space): remove hypothesis (#10185)

fpvandoorn committed 4 years ago

7a8a9146

chore(data/matrix/notation): split into 2 files (#10199)

urkud committed 4 years ago

7d240ce1

feat(analysis/special_functions/log): Relating `log`-inequalities and `exp`-inequalities (#10191)

YaelDillies committed 4 years ago

daac8545

feat(algebra/group/with_one): cleanup algebraic instances (#10194)

eric-wieser committed 4 years ago

169bb29d

feat(analysis/normed_space/continuous_affine_map): define bundled continuous affine maps (#10161)

ocfnash committed 4 years ago

56a9228f

feat(algebra/homology/image_to_kernel): homology.map_iso (#9978)

jcommelin committed 4 years ago

26c0c23e

chore(algebra/opposites): use `injective.*` constructors (#10200)

urkud committed 4 years ago

f18278de

feat(data/nat/basic): `a < a / b * b + b` (#10193)

YaelDillies committed 4 years ago

38caa506

feat(algebra/big_operators/order): Bound on a product from a pointwise bound (#10190)

YaelDillies committed 4 years ago

ebe7951d

fix(README): update specialties of maintainers (#10086)

jcommelin committed 4 years ago

be412c3d

Newer Older