leanprover-community/mathlib

Pull Requests Commits

Pull back `with_seminorms` along a linear inducing

ADedecker committed 3 years ago

a0ac76c6

`𝓝 0` in the topology induced by seminorms

ADedecker committed 3 years ago

85916a52

chore(model_theory/encoding): Improve the encoding of terms (#13532)

awainverse committed 3 years ago

a3a166bc

feat(topology/separation): Finite sets in T2 spaces (#12845)

vihdzp committed 3 years ago

d9a8d6e5

feat(analysis/inner_product_space/gram_schmidt_ortho): Gram-Schmidt Orthogonalization and Orthonormalization (#12857)

Biiiilly committed 3 years ago

8d351dc3

chore(algebra/big_operators/fin): golf finset.prod_range (#13535)

Ruben-VandeVelde committed 3 years ago

92f6eb6b

chore(analysis/normed_space/star): make an argument explicit (#13523)

eric-wieser committed 3 years ago

71b470f9

feat(*): `op_op_op_comm` lemmas (#13528)

YaelDillies committed 3 years ago

5038a4a9

chore(data/real/nnreal): add commuted version of `nnreal.mul_finset_sup` (#13512)

eric-wieser committed 3 years ago

cf5aea0a

chore(*/matrix): order `m` and `n` alphabetically (#13510)

eric-wieser committed 3 years ago

094b1f51

feat(analysis/calculus/specific_functions): trivial extra lemmas (#13516)

fpvandoorn committed 3 years ago

3ac979a2

feat(analysis): lemmas about nnnorm and nndist (#13498)

eric-wieser committed 3 years ago

70759ef9

feat(data/int/basic): add lemma `int.abs_le_one_iff` (#13513)

ocfnash committed 3 years ago

f06dca76

feat(category_theory/limits): add characteristic predicate for zero objects (#13511)

jcommelin committed 3 years ago

634eab10

feat(order/filter/n_ary): Add lemma equating map₂ to map on the product (#13490)

berndlosert committed 3 years ago

5dc8c1cf

fix(analysis/locally_convex/balanced_hull_core): minimize import (#13450)

ADedecker committed 3 years ago

8fa3263c

feat(order/cover): define `wcovby` (#13424)

fpvandoorn committed 3 years ago

ba6a9858

refactor(group_theory/group_action/big_operators): extract to a new file (#13340)

eric-wieser committed 3 years ago

8f7e10b8

fix(algebra/hom/units): better defeq in `is_unit.lift_right` (#13508)

alreadydone committed 3 years ago

3e78c237

feat(algebra/*/basic): add trivial lemmas (#13416)

ericrbg committed 3 years ago

5a4bae11

feat(order/succ_pred/basic): Intervals and `succ`/`pred` (#13486)

YaelDillies committed 3 years ago

9202b6d1

chore(docs): don't use deprecated is_subring (#13505)

kim-em committed 3 years ago

d19e8cb7

fix(category_theory/monoidal): increase class search depth in coherence tactic (#13413)

kim-em committed 3 years ago

828ef48c

feat(data/matrix/block): `matrix.block_diagonal` is a ring homomorphism (#13489)

eric-wieser committed 3 years ago

fb44330e

chore(algebra/monoid_algebra/basic): use the homomorphism typeclasses (#13389)

eric-wieser committed 3 years ago

eb22ba4f

chore(ring_theory/hahn_series, topology/locally_constant/algebra): add missing `non_unital_non_assoc_ring` instances (#13504)

j-loreaux committed 3 years ago

37d02d3d

chore(algebra/ring/{pi, prod}): fix errors in `ring_hom` for `pi` and `prod`. (#13501)

j-loreaux committed 3 years ago

3c20253b

chore(analysis/normed_space/finite_dimension): golf a proof (#13491)

eric-wieser committed 3 years ago

b54591f7

chore(data/nat/factorization): golf `dvd_iff_prime_pow_dvd_dvd` (#13473)

stuart-presnell committed 3 years ago

fd08afe3

feat(order/bounded_order): Strictly monotone functions preserve maximality (#13434)

YaelDillies committed 3 years ago

d89160b5

Older