Skip to content

Instantly share code, notes, and snippets.

View alok's full-sized avatar

Alok Singh alok

View GitHub Profile
author comments layout mathjax slug title
Alok Singh
true
post
true
noncommutative-3d-rotations
Exploring Non-Commutative 3D Rotations with Grassmann Algebra

People find rotation hard because when we try to visualize something, often we project it onto a 2D plane. But for rotations, this loses the plot because 2D rotations DO commute. In this post, we will (symbolically) explore this non-commutative nature of 3D rotations using Grassmann algebra in Julia. We'll use the Grassmann package to define rotors and demonstrate how the order of rotations matters in three-dimensional space.

import Mathlib
import Lean.Data.Parsec
import Batteries.Lean.HashMap
import Lean.Data.HashMap
import Lean.Util.Path
import Lean.Data.Rat
import LeanInf.Basic
-- set_option diagnostics true
theorem two_plus_two : 2 + 2 = 4 := rfl
@alok
alok / Lisp.lean
Created July 13, 2024 07:28
lisp parser in lean 4
import Lean
import Lean.Parser
import Mathlib
open Lean.Parsec
namespace Lisp
-- Lisp data types
inductive LispVal where
| Atom (name : String)
| List (elements : List LispVal)
@alok
alok / seventeen_dim.jl
Created May 4, 2024 08:39
5 and 17 dimensional rotations
# Reorganized code to focus on rotating a random 17-dimensional multivector and projecting it to 3D for visualization
using Grassmann
# Define the basis for 3D and 17D spaces
basis_3,basis_5,basis_17 = Λ(3), Λ(5), Λ(17)
# Define submanifolds for 3D and 17D spaces
V_3, V_5, V_17 = Submanifold(3), Submanifold(5), Submanifold(17)
@alok
alok / Printf.lean
Created December 10, 2023 08:06
Dependently typed printf
inductive Format :=
| Int (rest: Format) -- %d
| String (rest: Format) -- %s
| Other (char: Char) (rest: Format) -- %c
| End
def format : List Char -> Format
| ('%' :: 'd' :: cs) => .Int (format cs)
| ('%' :: 's' :: cs) => .String (format cs)
"""
Configuration example for ``ptpython``.
Copy this file to ~/.ptpython/config.py
"""
from __future__ import unicode_literals
from prompt_toolkit.keys import Keys
from ptpython.layout import CompletionVisualisation
from pygments.token import Token
{
"global": {
"check_for_updates_on_startup": true,
"show_in_menu_bar": true,
"show_profile_name_in_menu_bar": false
},
"profiles": [
{
"complex_modifications": {
"rules": [
{
"global": {
"check_for_updates_on_startup": true,
"show_in_menu_bar": true,
"show_profile_name_in_menu_bar": false
},
"profiles": [
{
"complex_modifications": {
"rules": [
{
"global": {
"check_for_updates_on_startup": true,
"show_in_menu_bar": true,
"show_profile_name_in_menu_bar": false
},
"profiles": [
{
"complex_modifications": {
"rules": [
{
"global": {
"check_for_updates_on_startup": true,
"show_in_menu_bar": true,
"show_profile_name_in_menu_bar": false
},
"profiles": [
{
"complex_modifications": {
"rules": [