Rot Z

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

noncomputable def CIV.rotZ (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The rotation Q_φ through the angle φ about the z-axis.

Equations

• CIV.rotZ φ x = ![Real.cos φ * x 0 - Real.sin φ * x 1, Real.sin φ * x 0 + Real.cos φ * x 1, x 2]