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
move is_interior_point
winstonyin committed 3 years ago
79c5482c
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
undergrad
winstonyin committed 3 years ago
98e9e448
add t0 as arg
winstonyin committed 3 years ago
bd1a59db
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
Terms Of Use Privacy Policy Refund Policy Impressum