leanprover-community/mathlib3

Pull Requests Commits

feat(ring_theory): equality of ideals from locally at each maximal ideal (#18142)

Vierkantor committed 2 years ago

c3350dbc

feat(analysis/convex/intrinsic): Intrinsic interior and frontier (#18027)

datokrat committed 2 years ago

9f26ebf2

feat(number_theory/zeta_values): evaluate critical values of Riemann zeta (#17994)

loefflerd committed 2 years ago

8cce17e5

feat(data/finset/sups): Set family operations (#17947)

YaelDillies committed 2 years ago

1990ff7e

feat(algebra/smul_with_zero): `a • b ≠ 0 → a ≠ 0` (#18086)

YaelDillies committed 2 years ago

12c24b79

feat(group_theory/subgroup/basic): Map a subgroup under an iso (#17775)

YaelDillies committed 2 years ago

cf8e77c6

chore(scripts): update nolints.txt (#18161)

leanprover-community-bot committed 2 years ago

d7943885

feat(data/finset/basic): add a `can_lift` instance (#18152)

urkud committed 2 years ago

f6a7bd6f

chore(data/list): golf, merge 2 files (#18120)

urkud committed 2 years ago

527e406f

feat(data/multiset/basic): `multiset.coe_eq_singleton` (#15910)

vihdzp committed 2 years ago

f3187269

chore(probability_mass_function/monad): Use standard `Union` notation (#18154)

dtumad committed 2 years ago

feb165c9

fix(*): fix typo in the word subtraction (#18145)

eric-wieser committed 2 years ago

d50b12ae

chore(*): remove some defeq abuse of `^` (#18136)

eric-wieser committed 2 years ago

7e7aaccf

chore(data/set/intervals/unordered_interval): Rename to `uIcc`/`uIoc` (#18104)

YaelDillies committed 2 years ago

9003f287

feat(data/polynomial): `adjoin_root.mk_ne_zero` lemmas (#18113)

alreadydone committed 2 years ago

1db04677

feat(geometry/euclidean/angle/unoriented/affine): more collinearity lemmas (#18069)

jsm28 committed 2 years ago

217daaf4

chore(linear_algebra/tensor_product): make more lemmas dsimp-eligible (#18140)

eric-wieser committed 2 years ago

b0c71237

chore(data/fin/basic): remove `fin.coe_of_nat_eq_mod` (#18131)

astrainfinita committed 2 years ago

008af8bb

refactor(linear_algebra/affine_space/*): make `affine_basis` more elementary (#18141)

hrmacbeth committed 2 years ago

579cdfe0

fix(tactic/{norm_num, abel}): do not do syntactic matches on typeclass instances (#18129)

eric-wieser committed 2 years ago

ec322deb

feat(topology/instances/ennreal): curried version of `ennreal.tsum_prod` (#18124)

dtumad committed 2 years ago

f8355031

feat(group_theory/group_action/support): Support under an action (#17055)

YaelDillies committed 2 years ago

36a35211

refactor(linear_algebra/tensor_product): make `lift f (x ⊗ₜ y) = f x y` true by `rfl` (#18121)

eric-wieser committed 2 years ago

657df433

feat(analysis/special_functions): Gaussian integral with complex parameter (#18090)

loefflerd committed 2 years ago

914cb177

feat(data/list/count): partially sync with multiset (#18125)

urkud committed 2 years ago

7c523cb7

feat(data/fin/vec_notation): add matrix.range_singleton and matrix.range_pair (#18112)

Multramate committed 2 years ago

5758ed34

chore(linear_algebra/tensor_product): generalize `tensor_tensor_tensor_comm_symm_tmul` (#18110)

eric-wieser committed 2 years ago

4568629f

refactor(data/fin/basic): fin refactor to use ne_zero (#18107)

ChrisHughes24 committed 2 years ago

0bd2ea37

chore(analysis/seminorm): golf (#18089)

urkud committed 2 years ago

fb987e22

chore(*): add mathlib4 synchronization comments (#18094)

leanprover-community-bot committed 2 years ago

be24ec5d

Newer Older