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

Open

Commits

initial commit

shadasali committed 5 years ago
Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

shadasali committed 5 years ago
Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

shadasali committed 5 years ago
Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

shadasali committed 5 years ago
Fix cyclic imports

shadasali committed 5 years ago
Move Lemmas to Trigonometric

shadasali committed 5 years ago
Fix to_additive in quotient_group

shadasali committed 5 years ago
Reorganize imports

shadasali committed 5 years ago
Rearrange angle_to_circle lemmas

shadasali committed 5 years ago
Fix Lint

shadasali committed 5 years ago
Remove the notation of pi

shadasali committed 5 years ago
Change dihedral_to_complex to dihedral_group.to_complex

shadasali committed 5 years ago
Fix dihedral and trigonometric files

shadasali committed 5 years ago
Fix lint

shadasali committed 5 years ago
cleanup

jcommelin committed 5 years ago
further golf

jcommelin committed 5 years ago
Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

eric-wieser committed 4 years ago
Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

eric-wieser committed 3 years ago
apply suggested golf

eric-wieser committed 3 years ago
fix style

eric-wieser committed 3 years ago
revert a golf that no longer works

eric-wieser committed 3 years ago
fix renames

eric-wieser committed 3 years ago
replace surjectivity with right-inverse

eric-wieser committed 3 years ago
fix import

YaelDillies committed 3 years ago

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

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

Open