`BookProof.ChapterRotaryPosition.norm_rotaryEncode` (omega : Fin n → ℝ) (p : ℝ) (q : EuclideanSpace ℂ (Fin n)) : ‖rotaryEncode omega p q‖ = ‖q‖

Initializing...

`BookProof.ChapterRotaryPosition.norm_rotaryEncode` (omega : Fin n → ℝ) (p : ℝ) (q : EuclideanSpace ℂ (Fin n)) : ‖rotaryEncode omega p q‖ = ‖q‖ · Prove2Me