refactor(algebra/star): replace `star_ring_aut` with `star` #9692
eric-wieser
wants to merge
87 commits into
master
from
eric-wieser/replace_conj_with_star
get rid of conj in is_R_or_C
018aae14
temporary fix for analysis/complex/basic
9a021915
add localized notation for complex conjugate
c5f5f40f
remove conj from complex
72a2b3d2
data/complex/module
61edb752
analysis/complex/basic
d8a85368
inner_product_space/basic
deec0a14
inner_product_space/dual
b0c65005
add big operator lemmas for ring equivs
a7b075f8
fix namespace
736db98b
Merge branch 'ring_equiv_big_operators' into replace_conj_with_star
d58bbe2d
use to_ring_hom in the proofs
d10cf093
Merge branch 'ring_equiv_big_operators' into replace_conj_with_star
9094f411
map_inv and map_div
9b93e766
map_pow
106d4401
data/complex/exponential
3274f295
analysis/complex/circle
72cfeb12
analysis/complex/isometry
8a924b23
put back conj_conj
bac4bf5f
analysis/complex/real_deriv
b31fd37f
add lemma star_ring_aut_self_apply, with conj_conj as an alias for it
6b24d7c8
docs
6d766984
remove redundant lemmas
d8aaf983
cleanup
798b7d10
remove is_R_or_C.conj_conj
0865caa0
Merge branch 'master' into replace_conj_with_star
83ab97e5
fix is_R_or_C
0bb6f08d
remove spurious alias
6f6e61c6
fix conj_conj
7f0ad384
fix inner_product_space/basic
9f10d630
inner_product_space/projection
dae82be0
pi_L2
e4015eb8
inner_product_space/dual
1e06acbc
clifford_algebra/equivs
28f18a44
more fixing in measure theory
a8e23590
add ring_equiv.map_fpow
6a4cdccf
oops
c686b93b
more fixes in fourier.lean
7e5816ba
add lemmas
146b9009
Merge branch 'beef_up_ring_equiv_api' into replace_conj_with_star
0ec5a10e
add comment explaining why `star_ring_aut_apply` is not a simp lemma
d322063b
documentation
c5b8e5c9
Add back simp
67ec54b3
change notation
acd6d684
fix
e6ea5936
rollback the changes to star/basic
4b418488
star_mul'
63b8bcc5
Add more lemmas about `star`
2bcbd9da
feat(algebra/star/basic): add some helper lemmas about `star`
fc5afc02
docstring
a726d862
lintfix
2d439648
one more
9faf0b69
Merge branch 'eric-wieser/star-lemmas' into eric-wieser/replace_conj_…
8afad7f2
fix
b14bc538
fix implicitness
87197ec1
fix
873c2267
fix
38ce9917
fix
1be3fb2c
more fixes
94c9ef9a
fix
7614f3f0
fix
76f510a9
fix
ade3bf73
fix with sorries
99e5ce72
chore(algebra/opposites): provide npow and gpow explicitly
32332b82
fix new diamond
070bfbaf
add lemmas
5de0e394
div_inv_monoid instance
5f99396a
last fix
2ccb9f73
Merge branch 'eric-wieser/op-gpow' into eric-wieser/star-lemmas
27625351
`star_gpow` and `star_fpow`
1fe1d6df
Merge branch 'master' into replace_conj_with_star
893fef1d
Merge branch 'eric-wieser/star-lemmas' of github.com:leanprover-commu…
4ac18d08
Merge remote-tracking branch 'origin/staging' into eric-wieser/star-l…
b8ea8781
Merge branch 'master' into eric-wieser/star-lemmas-gpow
3a3206f8
fix
4399b7e9
Merge remote-tracking branch 'origin/eric-wieser/star-lemmas-gpow' in…
c0caaad8
Merge branch 'master' into replace_conj_with_star
09389152
Update basic.lean
4d656d83
Merge remote-tracking branch 'origin/master' into eric-wieser/replace…
12e3403a
Merge branch 'eric-wieser/replace_conj_with_star' of github.com:leanp…
44559a8f
conj_to_ring_equiv -> abbreviation for star_ring_equiv
233433b0
Update src/data/complex/is_R_or_C.lean
35ac2507
remove redundant lemma
df42a2f6
Merge branch 'master' into replace_conj_with_star
b6d15288
fix data/complex/basic
2e1ac318
Merge remote-tracking branch 'origin/master' into replace_conj_with_star
4391f34a
Merge branch 'replace_conj_with_star' into eric-wieser/replace_conj_w…
579c7092
eric-wieser
changed the title 
Reviewers
No reviews
Assignees
No one assigned
Labels
RFC
merge-conflict
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub