leanprover-community/mathlib

Pull Requests Commits

dupuisf committed 4 years ago

49cf315c

implement code review comments + update module docstring

dupuisf committed 4 years ago

b502e7e4

Update src/linear_algebra/bilinear_map.lean

dupuisf committed 4 years ago

Verified 7a9f4f85

Update src/linear_algebra/bilinear_map.lean

dupuisf committed 4 years ago

Verified 3d08ad9d

missing docstring on def

dupuisf committed 4 years ago

7b93f041

remove duplicate arguments

dupuisf committed 4 years ago

782cf145

Merge branch 'master' into dupuisf/semilinear_bilinear_map2

dupuisf committed 4 years ago

2cf0b23a

now do it properly...

dupuisf committed 4 years ago

8dbaf0c7

semilinearize bilinear maps

dupuisf committed 4 years ago

46ff5f54

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

Older