Documentation
Atlas
.
AlgebraNotes
.
code
.
Isometries
Search
return to top
source
Imports
Init
Mathlib
Imported by
Isometries
.
Plane
Isometries
.
linearDet
Isometries
.
IsTranslation
Isometries
.
IsRotation
Isometries
.
IsReflection
Isometries
.
IsGlideReflection
Isometries
.
affine_decomp_aux
Isometries
.
plane_isometry_classification
Isometries
.
isometry_map_zero_isLinearMap
source
@[reducible, inline]
abbrev
Isometries
.
Plane
:
Type
Instances For
source
noncomputable def
Isometries
.
linearDet
(
f
:
Plane
≃ᵃⁱ[
ℝ
]
Plane
)
:
ℝ
Instances For
source
def
Isometries
.
IsTranslation
(
f
:
Plane
≃ᵃⁱ[
ℝ
]
Plane
)
:
Prop
Instances For
source
def
Isometries
.
IsRotation
(
f
:
Plane
≃ᵃⁱ[
ℝ
]
Plane
)
:
Prop
Instances For
source
def
Isometries
.
IsReflection
(
f
:
Plane
≃ᵃⁱ[
ℝ
]
Plane
)
:
Prop
Instances For
source
def
Isometries
.
IsGlideReflection
(
f
:
Plane
≃ᵃⁱ[
ℝ
]
Plane
)
:
Prop
Instances For
source
theorem
Isometries
.
affine_decomp_aux
(
f
:
Plane
≃ᵃⁱ[
ℝ
]
Plane
)
(
x
:
Plane
)
:
f
x
=
f
.
linearIsometryEquiv
x
+
f
0
source
theorem
Isometries
.
plane_isometry_classification
(
f
:
Plane
≃ᵃⁱ[
ℝ
]
Plane
)
:
IsTranslation
f
∨
IsRotation
f
∨
IsReflection
f
∨
IsGlideReflection
f
source
theorem
Isometries
.
isometry_map_zero_isLinearMap
{
n
:
ℕ
}
(
f
:
EuclideanSpace
ℝ
(
Fin
n
)
→
EuclideanSpace
ℝ
(
Fin
n
)
)
(
hf
:
Isometry
f
)
(
hf0
:
f
0
=
0
)
:
IsLinearMap
ℝ
f