leanprover-community/mathlib

Pull Requests Commits

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

refactor(geometry/euclidean/oriented_angle): split file (#17134)

jsm28 committed 3 years ago

54d1f9bb

docs(data/set/pointwise)/big_operators): Correct copyright (#17229)

YaelDillies committed 3 years ago

63645a77

feat(algebra/star/basic): basic lemmas for `star_ordered_ring` (#17218)

j-loreaux committed 3 years ago

27ac3e1a

chore(data/setoid/partition): use `set.finite` (#17228)

urkud committed 3 years ago

db46133c

feat(order/galois_connection): add 2 lemmas (#17221)

urkud committed 3 years ago

1417a74e

feat(topology/separation): add 2 lemmas about T2.5 spaces (#17224)

urkud committed 3 years ago

39cbe8db

feat(algebra/star/subalgebra): operations on `star_subalgebra`s (#17136)

j-loreaux committed 3 years ago

1bef0e2c

feat(analysis/complex): define `complex.unit_disc` (#17119)

urkud committed 3 years ago

8792402d

feat(order/filter): add several trivial lemmas (#17215)

urkud committed 3 years ago

282ca106

doc(group_theory/free_product): free not direct product (#17214)

kisonecat committed 3 years ago

5c60b7e3

feat(analysis/calculus/cont_diff): norms of iterated derivatives (#17150)

mcdoll committed 3 years ago

549f9850

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

leanprover-community-bot committed 3 years ago

45a856ca

feat(analysis/ODE/picard_lindelof): Add corollaries to ODE solution existence theorem (#16348)

winstonyin committed 3 years ago

f97c17d5

chore(data/nat/basic): split into two files, one not depending on the order hierarchy (#17174)

kim-em committed 3 years ago

a3240c4f

Newer Older