Jyxu/graded module #18308
alreadydone
merged
37 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
fixes
ba994c5b
Merge remote-tracking branch 'origin/master' into jyxu/graded_module
7c530deb
address reviews
71d4efd7
remove alias of set_like.has_graded_smul.smul_mem
798afc31
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Login to write a write a comment.
Login via GitHub