isometry): Homomorphism from Dihedral Group into Linear Isometries of C
#8559

Open

feat(analysis/complex/isometry): Homomorphism from Dihedral Group into Linear Isometries of C #8559

shadasali wants to merge 24 commits into master from Dihedral-Group-Lemmas

initial commit

ca36fd2c

shadasali added awaiting-review

github-actions added merge-conflict

eric-wieser commented on 2021-08-05

bryangingechen changed the title ~~feat(Analysis/Complex/Isometry): Homomorphism from Dihedral Group into Linear Isometries of C~~ feat(analysis/complex/isometry): Homomorphism from Dihedral Group into Linear Isometries of C 4 years ago

eric-wieser commented on 2021-08-05

pechersky commented on 2021-08-06

eric-wieser removed awaiting-review

eric-wieser added awaiting-author

Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

c15d35af

github-actions removed merge-conflict

Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

ebf08acf

Ruben-VandeVelde commented on 2021-08-08

Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

b29fca93

Fix cyclic imports

9b7e8513

Move Lemmas to Trigonometric

86380f4c

Fix to_additive in quotient_group

85ab6a08

Reorganize imports

28f2a300

Rearrange angle_to_circle lemmas

a2f4f4da

Fix Lint

3654e3cb

shadasali removed awaiting-author

shadasali added awaiting-review

Remove the notation of pi

82608974

eric-wieser commented on 2021-08-19

Change dihedral_to_complex to dihedral_group.to_complex

83c20553

jcommelin commented on 2021-08-26

jcommelin removed awaiting-review

jcommelin added awaiting-author

hrmacbeth commented on 2021-08-26

Fix dihedral and trigonometric files

0658578a

Fix lint

c8f4515b

jcommelin commented on 2021-08-28

cleanup

2327c3e0

further golf

df911cc9

eric-wieser commented on 2021-08-28

github-actions added merge-conflict

urkud commented on 2021-09-29

Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

b32781bd

github-actions removed merge-conflict

github-actions added merge-conflict

Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

fdb92dd2

apply suggested golf

5c230f5f

fix style

d805008d

revert a golf that no longer works

64a52c6c

fix renames

0955d063

replace surjectivity with right-inverse

79eb5555

YaelDillies removed merge-conflict

YaelDillies added t-algebra

fix import

cfeef526

kim-em added too-late

Reviewers

urkud

eric-wieser

jcommelin

hrmacbeth

Ruben-VandeVelde

pechersky

Assignees

No one assigned

Labels

awaiting-author t-algebra too-late

Milestone

No milestone

mathlib3 feat(analysis/complex/isometry): Homomorphism from Dihedral Group into Linear Isometries of C #8559 Open

feat(analysis/complex/isometry): Homomorphism from Dihedral Group into Linear Isometries of C #8559

mathlib3
feat(analysis/complex/isometry): Homomorphism from Dihedral Group into Linear Isometries of C
#8559

Open