leanprover-community/mathlib

Pull Requests Commits

RemyDegenne committed 3 years ago

a3678b5a

add tendsto_inf_principal_iff_seq_tendsto

RemyDegenne committed 3 years ago

d2320f2f

Merge remote-tracking branch 'origin/master' into RD_tendsto_seq

RemyDegenne committed 3 years ago

0fc4843e

feat(set_theory/cardinal): add `cardinal.range_nat_cast` (#17222)

urkud committed 3 years ago

a8a47a60

feat(algebra/order/upper_lower): Algebraic operations on upper sets (#16973)

YaelDillies committed 3 years ago

16279b04

feat(order/cover): add `wcovby_iff_le_and_eq_or_eq` (#17262)

eric-wieser committed 3 years ago

e0d82e89

feat(topology/continuous_on): add `tendsto_nhds_within_iff` (#17260)

RemyDegenne committed 3 years ago

34c828da

feat(group_theory/p_group): `card G = 1` or `p | card G`. (#17251)

tb65536 committed 3 years ago

1ee8921d

chore(data/finset/locally_finite): add more lemmas about one-sided intervals (#17033)

eric-wieser committed 3 years ago

bf07fdbb

docs(algebra/hom/group, tactic/push_neg): add docs to resolve some lint errors (#17225)

adomani committed 3 years ago

da8ded3f

Update src/topology/continuous_on.lean

RemyDegenne committed 3 years ago

Verified 7ceb5fe1

add tendsto_nhds_within_iff_seq_tendsto

RemyDegenne committed 3 years ago

34d38919

Merge remote-tracking branch 'origin/RD_tendsto_within' into RD_tendsto_seq

RemyDegenne committed 3 years ago

e970f07b

add tendsto_nhds_within_iff

RemyDegenne committed 3 years ago

65cdafc8

move(analysis/normed/order/lattice): Move from `analysis.normed_space.lattice_ordered_group` (#17255)

YaelDillies committed 3 years ago

7f5bf383

feat(group_theory/p_group): If `p ∤ n`, then the `n`th power map is a bijection (#17193)

tb65536 committed 3 years ago

2f18952b

feat(analysis/special_functions/trigonometric/angle): sign and π / 2 lemmas (#17129)

jsm28 committed 3 years ago

f8393c90

feat(group_theory/order_of_element): `order_of_pow_coprime` (#17252)

tb65536 committed 3 years ago

4ff481ad

chore(measure_theory/measure/finite_measure_weak_convergence): Change to probability theory notations. (#17231)

kkytola committed 3 years ago

8315f58e

chore(linear_algebra/projection): golf (#17244)

urkud committed 3 years ago

7a7d4dd4

chore(topology/algebra/module): add `protected` (#17247)

urkud committed 3 years ago

669eee94

feat(topology/semicontinuous): semicontinuity of conditional `supr`/`infi` (#17242)

ADedecker committed 3 years ago

02854ebf

move(analysis/normed/order/basic): Move from `analysis.normed_space.ordered` (#17239)

YaelDillies committed 3 years ago

76ec0e53

chore(*): consistently use R[X] notation for polynomials (#17044)

kim-em committed 3 years ago

62c0a4ef

chore(analysis/calculus/cont_diff): add missing lemmas and golfs (#17233)

mcdoll committed 3 years ago

2423ed87

feat(geometry/euclidean/angle/oriented/basic): `rotation_rotation` (#17235)

jsm28 committed 3 years ago

ae714fd5

docs(analysis/analytic/composition): fix typos (#17232)

urkud committed 3 years ago

c162b725

chore(analysis/normed/group/basic): Earlier `ℝ` lemmas (#16972)

YaelDillies committed 3 years ago

be61b02b

feat(data/set/basic): `symm_diff` lemmas (#17051)

YaelDillies committed 3 years ago

8a697e5d

chore(data/fintype/basic): golf, generalize to `Sort*` (#17227)

urkud committed 3 years ago

58debc0e

Older