leanprover-community/mathlib3

Pull Requests Commits

astrainfinita committed 2 years ago

9fef93cb

typeclass for relation

astrainfinita committed 2 years ago

e7b82fca

astrainfinita committed 2 years ago

24e24fc9

astrainfinita committed 2 years ago

e70b8c31

fix (what causes this?)

astrainfinita committed 2 years ago

8ba415bc

Merge branch 'FR_rel_iff' into FR_antisymmetrization

astrainfinita committed 2 years ago

729ae85e

`setoid_is_antisymm_rel`

astrainfinita committed 2 years ago

ba773e14

astrainfinita committed 2 years ago

e2c19d8a

Merge branch 'FR_rel_iff' into FR_antisymmetrization

astrainfinita committed 2 years ago

d693fd1a

astrainfinita committed 2 years ago

Verified 8978325d

astrainfinita committed 2 years ago

930b19f0

astrainfinita committed 2 years ago

7e516e59

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

astrainfinita committed 2 years ago

2153acf2

remove `rel_reflecting_class` `rel_iff_hom`

astrainfinita committed 2 years ago

790b0224

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

jsm28 committed 2 years ago

217daaf4

astrainfinita committed 2 years ago

b8aea421

astrainfinita committed 2 years ago

81bef5bd

Older