Commits leanprover-community/mathlib3

chore(group_theory/order_of_element): fix weird lemma name (#10245)

ericrbg committed 4 years ago

64289fe0

chore(set_theory/cardinal): fix name & reorder universes (#10236)

urkud committed 4 years ago

10d3d256

feat(algebra/module/linear_map,linear_algebra/alternating,linear_algebra/multilinear/basic): no_zero_smul_divisors instances (#10234)

jsm28 committed 4 years ago

7bdb6b39

feat(data/int/basic): coercion subtraction inequality (#10054)

cocohearts committed 4 years ago

a2810d97

feat(linear_algebra/determinant): alternating maps as multiples of determinant (#10233)

jsm28 committed 4 years ago

35d574e3

feast(ring_theory/norm): add norm_eq_prod_embeddings (#10226)

riccardobrasca committed 4 years ago

00d9b9f5

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

complete proof

sgouezel committed 4 years ago

bf2e22d1

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