leanprover-community/mathlib

Pull Requests Commits

ADedecker committed 3 years ago

2932505f

use letI instead of haveI

kex-y committed 3 years ago

ed790f31

generalize to polish spaces

kex-y committed 3 years ago

313e752c

RemyDegenne committed 3 years ago

435c990a

add `@[measurability]` and doc string

kex-y committed 3 years ago

ac4438c6

kex-y committed 3 years ago

ee521d1a

feat(data/matrix/notation): add `!![1, 2; 3, 4]` notation (#14991)

eric-wieser committed 3 years ago

83092fb4

feat(data/polynomial/unit_trinomial): An irreducibility criterion for unit trinomials (#14914)

tb65536 committed 3 years ago

01a18244

feat(data/polynomial/erase_lead): Characterization of polynomials of fixed support (#14741)

tb65536 committed 3 years ago

581b6940

feat(information_theory/hamming): add Hamming distance and norm (#14739)

linesthatinterlace committed 3 years ago

73402033

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

leanprover-community-bot committed 3 years ago

b06e32c2

refactor(logic/is_empty): tag `is_empty.forall_iff` and `is_empty.exists_iff` as `simp` (#14660)

vihdzp committed 3 years ago

5cb17dd1

refactor(topology/subset_properties): reformulate `is_clopen_b{Union,Inter}` in terms of `set.finite` (#15272)

urkud committed 3 years ago

ea13c1cf

feat(data/finsupp/basic): graph of a finitely supported function (#15197)

vihdzp committed 3 years ago

2a325960

feat(algebra/parity): more general odd.pos (#15186)

ericrbg committed 3 years ago

c6014bd2

refactor(topology/separation): rename `regular_space` to `t3_space` (#15169)

urkud committed 3 years ago

ede73b25

refactor(data/matrix/basic): add matrix.of for type casting (#14992)

eric-wieser committed 3 years ago

6c351a8f

feat(topology/maps): more `iff` lemmas (#15165)

urkud committed 3 years ago

834488ee

feat(analysis/special_functions/pow): drop an assumption in `is_o_log_rpow_rpow_at_top` (#15164)

urkud committed 3 years ago

7bd47556

feat(ring_theory/bezout): Define Bézout rings. (#15091)

erdOne committed 3 years ago

3543262a

feat(algebra/ring/{pi, prod, opposite}): add basic defs for non_unital_ring_hom (#13958)

j-loreaux committed 3 years ago

ece3044a

chore(data/set/finite): golf some proofs (#15273)

urkud committed 3 years ago

55db0722

feat(analysis/special_functions/trigonometric/angle): equality of twice angles (#14988)

jsm28 committed 3 years ago

7251bbf7

feat(data/nat/parity): `nat.bit1_div_bit0` (#15268)

tb65536 committed 3 years ago

89a80e67

chore(*): improve some definitional equalities (#15083)

urkud committed 3 years ago

9c400932

feat(data/nat/basic): add `strong_sub_recursion` and `pincer_recursion` (#15061)

stuart-presnell committed 3 years ago

eb091f87

feat(set_theory/game/pgame): strengthen `lf_or_equiv_of_le` to `lt_or_equiv_of_le` (#15255)

vihdzp committed 3 years ago

13f04ec6

feat(algebra/module/torsion): `R/I`-module structure on `M/IM`. (#15092)

erdOne committed 3 years ago

0d659de3

feat(order/order_iso_nat): generalize `well_founded.monotone_chain_condition` to preorders (#15073)

vihdzp committed 3 years ago

fef5124e

feat(representation_theory/character): formula for the dimension of the invariants in terms of the character (#15084)

antoinelab01 committed 3 years ago

119e166b

Older