leanprover-community/mathlib

Pull Requests Commits

feat(linear_algebra/bilinear_form): add lemmas (#10353)

riccardobrasca committed 4 years ago

276ab17f

chore(measure_theory/group/basic): drop measurability assumption (#10367)

urkud committed 4 years ago

6f793bb0

chore(category_theory/filtered): slightly golf two proofs (#10368)

Ruben-VandeVelde committed 4 years ago

e14e87ae

feat(linear_algebra/bilinear_form): add lemmas about congr (#10362)

eric-wieser committed 4 years ago

c7441af1

chore(analysis/inner_product_space/projection): typeclass inference for completeness (#10357)

hrmacbeth committed 4 years ago

568435cb

chore(analysis/mean_inequalities): split mean_inequalities into two files (#10355)

RemyDegenne committed 4 years ago

d5c2b34c

feat(finset/basic): Adding `list.to_finset_union` and `list.to_finset_inter` (#10351)

stuart-presnell committed 4 years ago

60363a4e

lint(*): curly braces linter (#10280)

jcommelin committed 4 years ago

8f6fd1b6

feat(order/imp): define `lattice.imp` and `lattice.biimp` (#10327)

urkud committed 4 years ago

2bdadb4f

feat(combinatorics/set_family/shadow): Shadow of a set family (#10223)

YaelDillies committed 4 years ago

0a2a9229

feat(topology/metric_space/hausdorff_distance): add definition and lemmas about open thickenings of subsets (#10188)

kkytola committed 4 years ago

7fec4014

feat(number_theory/divisors): mem_divisors_self (#10359)

ericrbg committed 4 years ago

bce0ede7

refactor(linear_algebra/bilinear_form): Change namespace of is_refl, is_symm, and is_alt (#10338)

mcdoll committed 4 years ago

8f7971ae

feat(data/fin/basic): add lemmas about fin.cast (#10329)

eric-wieser committed 4 years ago

698eb1e3

feat(topology/uniform_space): properties of uniform convergence (#9958)

fpvandoorn committed 4 years ago

9fa14a60

feat(number_theory): define the class number (#9071)

Vierkantor committed 4 years ago

d6b83d87

feat(dynamics): define `{mul,add}_action.is_minimal` (#10311)

urkud committed 4 years ago

f7807881

feat(linear_algebra/sesquilinear_form): Add is_refl for sesq_form.is_alt (#10341)

mcdoll committed 4 years ago

d36f17f8

feat(linear_algebra/determinant): the determinant associated to the standard basis of the free module is the usual matrix determinant (#10278)

ocfnash committed 4 years ago

7f4b91b0

feat(field_theory): define the field of rational functions `ratfunc` (#9563)

Vierkantor committed 4 years ago

e20af159

chore(order/filter/basic): add 2 trivial `simp` lemmas (#10344)

urkud committed 4 years ago

f01399c4

feat(algebra/order/archimedean): upgrade some `∃` to `∃!` (#10343)

urkud committed 4 years ago

1181c990

chore(*): clean up some unused open statements and extra simps (#10342)

alexjbest committed 4 years ago

30abde68

feat(data/fin/basic): extract `div_nat` and `mod_nat` from `fin_prod_fin_equiv` (#10339)

eric-wieser committed 4 years ago

979f0e83

chore(ring_theory/subring): fix stale docstring (#10340)

ocfnash committed 4 years ago

bd80b339

feat(analysis/calculus/times_cont_diff): continuous affine maps are smooth (#10335)

ocfnash committed 4 years ago

9264f302

feat(data/nat/lattice): add ```Inf_add``` lemma (#10008)

SymmetryUnbroken committed 4 years ago

bff69c9f

feat(algebra/homology/exact): preadditive.exact_iff_exact_of_iso (#9979)

jcommelin committed 4 years ago

ddb6c75f

chore(linear_algebra/pi_tensor_product): add reindex_reindex (#10336)

eric-wieser committed 4 years ago

90740956

feat(logic/relation): induction principles for `trans_gen` (#10331)

fpvandoorn committed 4 years ago

a0f2c47f

Newer Older