Jyxu/graded module #18310
alreadydone
merged
90 commits into
jjaassoonn/graded_module
from
jyxu/graded_module
feat(algebra/triv_sq_zero_ext): lemmas about pow, and ring structure …
7c3780f6
feat (analysis/integrals): integral of x * (1 + x^2)^t (#18201)
15a07a99
chore(*): add mathlib4 synchronization comments (#18202)
cc70d914
chore(ring_theory/adjoin_root): fix timeout by writing out `simps` ma…
97586a95
refactor(geometry/euclidean/angle/unoriented/basic): split out confor…
df78eae5
refactor(geometry/euclidean/angle/oriented/basic): split out rotation…
fb319896
fix(geometry/euclidean/circumcenter): fix `fintype_finite` lint error…
509de852
chore(analysis/normed_space/continuous_linear_map): fix docs typo (#1…
e0e2f10d
fix(tactic/ring): perform definitional rather than syntactic matches …
c1ada9d1
feat(data/real/sqrt): add sqrt_div' lemma (#18216)
3b9e2ef2
chore(scripts): update nolints.txt (#18223)
1684fd2a
refactor(analysis/normed/group/hom): split (#18219)
3c422528
feat(topology/algebra/infinite_sum): Generalized lemmas for `add_comm…
b84da9c8
chore(analysis/complex/cauchy_integral): squeeze simp (#18225)
e94cd75f
feat(analysis/special_functions/pow): interaction between `cpow` and …
9292ecc2
chore(data/nat/digits): golf, use seemingly weaker assumptions (#18203)
2609ad04
chore(data/fintype/vector, logic/equiv/list): split (#18226)
78314d08
feat(algebra/group/basic): reduce additivity checks to one case (#18080)
4060545f
fix(topology/basic): docstring typo (#18229)
1126441d
chore(group_theory/subgroup/basic): split out some self-contained sec…
0f6670b8
feat(data/list/alist): recursion on `alist` using `insert` (#15434)
f808feb6
chore(*): detect blobs in port_status (#18237)
3f0c8b32
feat(special_functions/gamma): Bohr-Mollerup theorem (#18188)
52e2fbbd
feat(data/finset/basic): `finset.to_list_eq_singleton_iff` (#18236)
68cc4218
fix(data/finsupp/basic): add missing `decidable` arguments in lemma s…
2445c98a
feat(linear_algebra/dual): lemmas (#18228)
2d3f0c84
chore(analysis/convex/topology): split (#18187)
a63928c3
chore(group_theory/subgroup/basic): split out finiteness (#18242)
6f9f3636
feat(topology/order/lower_topology): Introduce the lower topology on …
38fe3f3c
refactor(set_theory/ordinal/arithmetic): fix `rank` universes (#18239)
2751ae21
feat(algebra/group/inj_surj): Missing transfer instances (#18247)
d23418e0
feat(data/sym/sym2): `set_like` instance (#17154)
e1503e02
feat(analysis/bounded_variation): define `variation_on_from_to` (#18040)
d6fad0e5
fix(linear_algebra/basis): add missing decidable arguments in lemmas …
f2edd790
fixes
ba994c5b
Merge remote-tracking branch 'origin/master' into jyxu/graded_module
7c530deb
address reviews
71d4efd7
refactor(order/filter/basic): drop a lemma (#18254)
02315164
remove alias of set_like.has_graded_smul.smul_mem
798afc31
refactor(group_theory/monoid_localization): flip the direction of mul…
831c4940
feat(set_theory/zfc/basic): better docs on `univ_not_mem_univ` (#18234)
800d3d45
refactor(data/finsupp/basic): split out alist results (#18250)
ae5357f9
chore(order/filter/basic): fix 2 typos (#18253)
fc3dc609
fix(order/filter/basic): fix a diamond (#18255)
71efed1b
feat(data/nat/hyperoperation): Defined hyperoperation and added relat…
386c02e7
feat(special_functions/trigonometric/bounds): Add the inequality `cos…
9df54c1b
chore(analysis/von_neumann_algebra/basic): add missing API lemmas (#1…
160ef3e3
refactor(data/set/finite): reduce imports (#18245)
1f0096e6
chore(field_theory/minpoly/*): replace `gcd_monoid.lean` by `is_integ…
2032a878
doc(computability/primrec): remove doc nolints (#16018)
959c3b69
feat(data/tree): Add definitions about binary trees; special support …
ed989ff5
fix(*/finsupp/*): add missing decidable arguments in lemma statements…
6e492fdb
chore(*): add mathlib4 synchronization comments (#18218)
327c3c0d
chore(data/finsupp/defs): move lemmas out of the single section which…
33694ffd
refactor(data/nat/parity): reduce imports, add/delete lemmas (#18221)
8631e2d5
feat(algebraic_geometry/elliptic_curve/weierstrass): define a basis f…
808ea4eb
feat(linear_algebra/dual): more about dual annihilator, some refactor…
68626536
refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade i…
468b141b
chore(scripts): update nolints.txt (#18273)
0be37584
doc(order/game_add): improve docstrings (#18269)
6f870fad
feat(ring_theory/localization): localization of a basis, again (#18261)
b69c9a77
chore(*): add mathlib4 synchronization comments (#18272)
63f84d91
feat(tactic/simps): store generated lemmas in attribute (#17964)
e3d9ab8f
chore(test/gmonoid): Add a test of the gmonoid API (#18197)
bbd198e1
feat(topology/algebra): add converse to tendsto.mul (#18276)
a81201cc
fix(*): add missing `classical` tactics and `decidable` arguments (#1…
6623e6af
refactor(topology): move `pcontinuous` etc to a new file (#18288)
2987594a
chore(*): add mathlib4 synchronization comments (#18283)
4d392a6c
chore(*): golf (#18111)
f974ae84
feat(algebra/order/ring/with_top): ring covariance & ordered ring typ…
e7e2ba8a
feat(data/nat/with_bot): `n < m → n + 1 ≤ m` (#18174)
12665d36
feat(data/pequiv,order/initial_seg): use `fun_like`, `embedding_like`…
7c3269ca
feat(ring_theory/dedekind_domain): localizing a Dedekind domain at a …
926daa81
feat(measure_theory/integrals): better interval_integral_pos (#18278)
9ac58f08
feat(order/game_add): add more lemmas (#16082)
4d756328
feat(algebra/order/kleene) : Kleene algebras (#17965)
a239cd3e
feat(analysis/constant_speed): define constant speed functions and pr…
168eeff2
feat(set_theory/zfc/basic): more basic simp/ext lemmas (#18233)
996b0ff9
feat(analysis/calculus/cont_diff): Prove that `fderiv_within` is `C^n…
27f315c5
feat(geometry/manifold/mfderiv): more arithmetic (#17793)
f93c1193
refactor(number_theory/primorial): split the proof, golf it (#18238)
966e0cf0
feat(analysis/special_functions/gamma): monotonicity of the Gamma fun…
0ee3e6f5
chore(set_theory/game/nim): golf `grundy_value_nim_add_nim` (#15878)
397a33d9
feat(algebra/homology/opposite): add opposite complexes (#18144)
8c75ef35
chore(set_theory/zfc/basic): `mem_empty` → `not_mem_empty` (#18262)
7a1cc03e
feat(special_functions/integrals): integral of `cos(a * x)` for `a` c…
2ef3da38
feat(data/real/pi): refactor Wallis formula for pi (#18280)
9b94375a
feat(set_theory/zfc/basic): `pSet.equiv.comm` (#18297)
cd45082b
feat(number_theory/kummer_dedekind): the return of the Dedekind-Kumme…
f7fc89d5
Merge remote-tracking branch 'origin/master' into jyxu/graded_module
7e1ac316
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Login to write a write a comment.
Login via GitHub