leanprover-community/mathlib3

Pull Requests Commits

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

feat(data/fintype/basic): add fin_injective (#10330)

eric-wieser committed 4 years ago

65ff54c7

feat(linear_algebra/determinant): linear coordinates are ratio of determinants (#10261)

ocfnash committed 4 years ago

93047c52

feat(topology/homotopy/fundamental_groupoid): The functor from `Top` to `Groupoid` (#10195)

shingtaklam1324 committed 4 years ago

7ccc7ae6

feat(data/fintype): computable trunc bijection from fin (#10141)

kmill committed 4 years ago

9c03e9dc

feat(ring_theory/subring): weaken typeclass assumption for `units.pos_subgroup` (#10332)

ocfnash committed 4 years ago

7b607682

feat(data/pi): Composition of addition/subtraction/... of functions (#10305)

YaelDillies committed 4 years ago

7803884e

feat(category_theory/limits): Random results about limits. (#10285)

erdOne committed 4 years ago

43ef5787

feat(data/finset/basic): A finset has card two iff it's `{x, y}` for some `x ≠ y` (#10252)

YaelDillies committed 4 years ago

1a47cfc7

Newer Older