Commits leanprover-community/mathlib

feat(algebra/lie/classical): Use computable matrix inverses where possible (#10218)

eric-wieser committed 4 years ago

11ced180

refactor(data/nat/interval): simp for Ico_zero_eq_range (#10211)

BoltonBailey committed 4 years ago

86146152

feat(order/bounded_lattice): a couple of basic instances about with_bot still not having a top if the original preorder didn't and vice versa (#10215)

alexjbest committed 4 years ago

0b093e6a

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

leanprover-community-bot committed 4 years ago

6af6f670

doc(data/finset/fold): fix typo (#10239)

ericrbg committed 4 years ago

9d49c4ad

chore(linear_algebra/basic): remove a duplicate proof, generalize map_span_le (#10219)

eric-wieser committed 4 years ago

223f6590

chore(*): bump to Lean 3.35.1 (#10237)

kim-em committed 4 years ago

424012aa

chore(topology/algebra/mul_action): define `has_continuous_vadd` using `to_additive` (#10227)

hrmacbeth committed 4 years ago

440163b4

feat(linear_algebra/matrix/nonsingular_inverse): add invertible_equiv_det_invertible (#10222)

eric-wieser committed 4 years ago

2e4813dd

chore(set_theory/cardinal): more simp, fix LHS/RHS (#10212)

urkud committed 4 years ago

1519cd77

feat(analysis/convex/specific_functions): Strict convexity of `exp`, `log` and `pow` (#10123)

YaelDillies committed 4 years ago

66dea297

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