leanprover-community/mathlib3

Pull Requests Commits

awainverse committed 3 years ago

946c7f27

awainverse committed 3 years ago

cafac86b

awainverse committed 3 years ago

3e508ae7

awainverse committed 3 years ago

3bd2e47a

awainverse committed 3 years ago

1acb8cb1

awainverse committed 3 years ago

4bafeb15

awainverse committed 3 years ago

48f65185

chore(topology/algebra/mul_action): rename type variables (#12020)

urkud committed 3 years ago

8a286af6

awainverse committed 3 years ago

a6c737b8

awainverse committed 3 years ago

0a9f5219

awainverse committed 3 years ago

db3712ee

chore(topology/algebra/module/basic): remove two duplicate lemmas (#12072)

eric-wieser committed 3 years ago

e8156757

feat(mv_polynomial/supported): restrict_to_vars (#12043)

robertylewis committed 3 years ago

a26d17fc

feat(analysis/complex/cauchy_integral, analysis/analytic/basic): entire functions have power series with infinite radius of convergence (#11948)

j-loreaux committed 3 years ago

62297cf0

chore(linear_algebra/affine_space/affine_map,topology/algebra/continuous_affine_map): generalized scalar instances (#11978)

eric-wieser committed 3 years ago

22fdf47e

feat(algebra/order/monoid): add simp lemmas (#12030)

mariainesdff committed 3 years ago

32beebbc

refactor(algebra/group/basic): add extra typeclasses for negation (#11960)

eric-wieser committed 3 years ago

75421198

feat(model_theory/terms_and_formulas): Define satisfiability and semantic equivalence of formulas (#11928)

awainverse committed 3 years ago

d24792c6

feat(algebra/star/self_adjoint): define skew-adjoint elements of a star additive group (#12013)

dupuisf committed 3 years ago

6dfb24cf

feat(analysis/special_functions/trigonometric/angle): `coe_pi_add_coe_pi` (#12064)

jsm28 committed 3 years ago

06e6b35d

feat(algebra/big_operators): formula for product of sums to n+1 (#12042)

robertylewis committed 3 years ago

daf2989a

chore(topology/uniform_space): use weaker TC assumptions (#12066)

urkud committed 3 years ago

6a09cd06

feat(topology/algebra): relax some `Type*` assumptions to `Sort*` (#12058)

ADedecker committed 3 years ago

eeb29569

feat (analysis/normed_space/spectrum): prove Gelfand's formula for the spectral radius (#11916)

j-loreaux committed 3 years ago

b0fe9723

feat(category_theory): separators and detectors (#11880)

TwoFX committed 3 years ago

d76ac2e0

feat(combinatorics/simple_graph/connectivity): add functions to split walks and to create paths (#11095)

kmill committed 3 years ago

ff2c9dc3

move(data/nat/choose/bounds): Move from `combinatorics.choose.bounds` (#12051)

YaelDillies committed 3 years ago

5027b283

feat(data/{list,multiset,finset}/nat_antidiagonal): add lemmas to remove elements from head and tail of antidiagonal (#12028)

kmill committed 3 years ago

52aaf173

feat(data/equiv,logic/embedding): add `can_lift` instances (#12049)

urkud committed 3 years ago

c0c673ab

feat(analysis/specific_limits): add `tendsto_zero_smul_of_tendsto_zero_of_bounded` (#12039)

ecstatic-morse committed 3 years ago

c686fcc1

Older