lean-ga / geometric_algebra.nursery.chisolm

@[class]

structure geometric_algebra (G₀ : Type u_1) [field G₀] (G₁ : Type u_2) [add_comm_group G₁] [module G₀ G₁] (G : Type u_3) [ring G] [algebra G₀ G] :

Type (max u_2 u_3)

f₁ : G₁ →+ G
vec_sq_scalar : ∀ (v : G₁), ∃ (k : G₀), ⇑(geometric_algebra.f₁ G₀) v * ⇑(geometric_algebra.f₁ G₀) v = ⇑(algebra_map G₀ G) k

Instances of this typeclass

Instances of other typeclasses for geometric_algebra

geometric_algebra.has_sizeof_inst

source

inductive geometric_algebra.blade {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

ℕ → Type u

scalar : Π {G₀ : Type u} [_inst_1 : field G₀] {G₁ : Type u} [_inst_2 : add_comm_group G₁] [_inst_3 : module G₀ G₁], G₀ → geometric_algebra.blade 0
vector : Π {G₀ : Type u} [_inst_1 : field G₀] {G₁ : Type u} [_inst_2 : add_comm_group G₁] [_inst_3 : module G₀ G₁], G₁ → geometric_algebra.blade 1
graded : Π {G₀ : Type u} [_inst_1 : field G₀] {G₁ : Type u} [_inst_2 : add_comm_group G₁] [_inst_3 : module G₀ G₁] {n : ℕ}, G₁ → geometric_algebra.blade (n + 1) → geometric_algebra.blade (n + 2)

Instances for geometric_algebra.blade

source

@[protected, instance]

def geometric_algebra.blade.g0_coe {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

has_coe_t G₀ (geometric_algebra.blade 0)

Equations

geometric_algebra.blade.g0_coe = {coe := geometric_algebra.blade.scalar _inst_3}

source

@[protected, instance]

def geometric_algebra.blade.g1_coe {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

has_coe_t G₁ (geometric_algebra.blade 1)

Equations

geometric_algebra.blade.g1_coe = {coe := geometric_algebra.blade.vector _inst_3}

source

def geometric_algebra.blade.zero {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] (n : ℕ) :

geometric_algebra.blade n

Equations

source

@[protected, instance]

def geometric_algebra.blade.has_zero {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

has_zero (geometric_algebra.blade n)

Equations

geometric_algebra.blade.has_zero = {zero := geometric_algebra.blade.zero n}

source

@[protected, instance]

def geometric_algebra.blade.r0_has_one {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

has_one (geometric_algebra.blade 0)

Equations

geometric_algebra.blade.r0_has_one = {one := ↑1}

source

def geometric_algebra.blade.r0_add {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] (a b : geometric_algebra.blade 0) :

geometric_algebra.blade 0

Equations

a.r0_add b = a.cases_on (λ (a' : G₀) (a_1 : 0 = 0) (H_2 : a == geometric_algebra.blade.scalar a'), eq.rec (b.cases_on (λ (b' : G₀) (a : 0 = 0) (H_2 : b == geometric_algebra.blade.scalar b'), eq.rec (geometric_algebra.blade.scalar (a' + b')) _) (λ (b_1 : G₁) (a : 0 = 1), nat.no_confusion a) (λ {b_n : ℕ} (b_ᾰ : G₁) (b_ᾰ_1 : geometric_algebra.blade (b_n + 1)) (a : 0 = (b_n.add (1.add 0)).succ), nat.no_confusion a) geometric_algebra.blade.r0_add._proof_2 _) _) (λ (a_1 : G₁) (a_2 : 0 = 1), nat.no_confusion a_2) (λ {a_n : ℕ} (a_ᾰ : G₁) (a_ᾰ_1 : geometric_algebra.blade (a_n + 1)) (a_1 : 0 = (a_n.add (1.add 0)).succ), nat.no_confusion a_1) geometric_algebra.blade.r0_add._proof_5 _

source

@[protected, instance]

def geometric_algebra.blade.r0_has_add {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

has_add (geometric_algebra.blade 0)

Equations

geometric_algebra.blade.r0_has_add = {add := geometric_algebra.blade.r0_add _inst_3}

source

def geometric_algebra.blade.r1_add {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] (a b : geometric_algebra.blade 1) :

geometric_algebra.blade 1

Equations

a.r1_add b = a.cases_on (λ (a_1 : G₀) (a_2 : 1 = 0), nat.no_confusion a_2) (λ (a_1 : G₁) (a_2 : 1 = 1) (H_2 : a == geometric_algebra.blade.vector a_1), eq.rec (b.cases_on (λ (b_1 : G₀) (a : 1 = 0), nat.no_confusion a) (λ (b_1 : G₁) (a : 1 = 1) (H_2 : b == geometric_algebra.blade.vector b_1), eq.rec (geometric_algebra.blade.vector (a_1 + b_1)) _) (λ {b_n : ℕ} (b_ᾰ : G₁) (b_ᾰ_1 : geometric_algebra.blade (b_n + 1)) (a : 1 = (b_n.add (1.add 0)).succ), nat.no_confusion a (λ (a : 0 = (b_n.add 0).succ), nat.no_confusion a)) geometric_algebra.blade.r1_add._proof_2 _) _) (λ {a_n : ℕ} (a_ᾰ : G₁) (a_ᾰ_1 : geometric_algebra.blade (a_n + 1)) (a_1 : 1 = (a_n.add (1.add 0)).succ), nat.no_confusion a_1 (λ (a_1 : 0 = (a_n.add 0).succ), nat.no_confusion a_1)) geometric_algebra.blade.r1_add._proof_5 _

source

@[protected, instance]

def geometric_algebra.blade.r1_has_add {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

has_add (geometric_algebra.blade 1)

Equations

geometric_algebra.blade.r1_has_add = {add := geometric_algebra.blade.r1_add _inst_3}

source

inductive geometric_algebra.hom_mv {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

ℕ → Type u

scalar : Π {G₀ : Type u} [_inst_1 : field G₀] {G₁ : Type u} [_inst_2 : add_comm_group G₁] [_inst_3 : module G₀ G₁], geometric_algebra.blade 0 → geometric_algebra.hom_mv 0
vector : Π {G₀ : Type u} [_inst_1 : field G₀] {G₁ : Type u} [_inst_2 : add_comm_group G₁] [_inst_3 : module G₀ G₁], geometric_algebra.blade 1 → geometric_algebra.hom_mv 1
graded : Π {G₀ : Type u} [_inst_1 : field G₀] {G₁ : Type u} [_inst_2 : add_comm_group G₁] [_inst_3 : module G₀ G₁] {n : ℕ}, list (geometric_algebra.blade n.succ.succ) → geometric_algebra.hom_mv n.succ.succ

Instances for geometric_algebra.hom_mv

geometric_algebra.hom_mv.has_sizeof_inst
geometric_algebra.hom_mv.has_blade_coe
geometric_algebra.hom_mv.has_g0_coe
geometric_algebra.hom_mv.has_g1_coe
geometric_algebra.hom_mv.has_zero
geometric_algebra.hom_mv.r0_has_one
geometric_algebra.hom_mv.has_add
geometric_algebra.mv.has_hom_mv_coe

source

def geometric_algebra.hom_mv.coe {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

geometric_algebra.blade n → geometric_algebra.hom_mv n

Equations

source

@[protected, instance]

def geometric_algebra.hom_mv.has_blade_coe {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {r : ℕ} :

has_coe (geometric_algebra.blade r) (geometric_algebra.hom_mv r)

Equations

geometric_algebra.hom_mv.has_blade_coe = {coe := geometric_algebra.hom_mv.coe r}

source

@[protected, instance]

def geometric_algebra.hom_mv.has_g0_coe {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

has_coe_t G₀ (geometric_algebra.hom_mv 0)

Equations

geometric_algebra.hom_mv.has_g0_coe = {coe := λ (s : G₀), geometric_algebra.hom_mv.coe ↑s}

source

@[protected, instance]

def geometric_algebra.hom_mv.has_g1_coe {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

has_coe_t G₁ (geometric_algebra.hom_mv 1)

Equations

geometric_algebra.hom_mv.has_g1_coe = {coe := λ (s : G₁), geometric_algebra.hom_mv.coe ↑s}

source

@[protected, instance]

def geometric_algebra.hom_mv.has_zero {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

has_zero (geometric_algebra.hom_mv n)

Equations

geometric_algebra.hom_mv.has_zero = {zero := ↑0}

source

@[protected, instance]

def geometric_algebra.hom_mv.r0_has_one {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

has_one (geometric_algebra.hom_mv 0)

Equations

geometric_algebra.hom_mv.r0_has_one = {one := ↑1}

source

def geometric_algebra.hom_mv.add {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

geometric_algebra.hom_mv n → geometric_algebra.hom_mv n → geometric_algebra.hom_mv n

Equations

(geometric_algebra.hom_mv.graded a).add (geometric_algebra.hom_mv.graded b) = geometric_algebra.hom_mv.graded (a ++ b)
(geometric_algebra.hom_mv.vector a).add (geometric_algebra.hom_mv.vector b) = geometric_algebra.hom_mv.vector (a + b)
(geometric_algebra.hom_mv.scalar a).add (geometric_algebra.hom_mv.scalar b) = geometric_algebra.hom_mv.scalar (a + b)

source

@[protected, instance]

def geometric_algebra.hom_mv.has_add {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

has_add (geometric_algebra.hom_mv n)

Equations

geometric_algebra.hom_mv.has_add = {add := geometric_algebra.hom_mv.add n}

source

inductive geometric_algebra.multivector {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

ℕ → Type u

scalar : Π {G₀ : Type u} [_inst_1 : field G₀] {G₁ : Type u} [_inst_2 : add_comm_group G₁] [_inst_3 : module G₀ G₁], geometric_algebra.hom_mv 0 → geometric_algebra.multivector 0
augment : Π {G₀ : Type u} [_inst_1 : field G₀] {G₁ : Type u} [_inst_2 : add_comm_group G₁] [_inst_3 : module G₀ G₁] {n : ℕ}, geometric_algebra.multivector n → geometric_algebra.hom_mv n.succ → geometric_algebra.multivector n.succ

Instances for geometric_algebra.multivector

geometric_algebra.multivector.has_sizeof_inst
geometric_algebra.mv.mv_has_zero
geometric_algebra.mv.mv_has_one
geometric_algebra.mv.has_hom_mv_coe
geometric_algebra.mv.has_g0_coe_t
geometric_algebra.mv.has_g1_coe_t
geometric_algebra.mv.has_augment_coe
geometric_algebra.mv.has_g0_coe_n
geometric_algebra.mv.has_g1_coe_n
geometric_algebra.mv.has_add

source

def geometric_algebra.mv.mv_zero {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] (n : ℕ) :

geometric_algebra.multivector n

Equations

source

def geometric_algebra.mv.mv_one {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] (n : ℕ) :

geometric_algebra.multivector n

Equations

source

@[protected, instance]

def geometric_algebra.mv.mv_has_zero {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

has_zero (geometric_algebra.multivector n)

Equations

geometric_algebra.mv.mv_has_zero = {zero := geometric_algebra.mv.mv_zero n}

source

@[protected, instance]

def geometric_algebra.mv.mv_has_one {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

has_one (geometric_algebra.multivector n)

Equations

geometric_algebra.mv.mv_has_one = {one := geometric_algebra.mv.mv_one n}

source

def geometric_algebra.mv.hom_mv_coe {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

geometric_algebra.hom_mv n → geometric_algebra.multivector n

Equations

geometric_algebra.mv.hom_mv_coe = λ (b : geometric_algebra.hom_mv n.succ), (geometric_algebra.mv.mv_zero n).augment b
geometric_algebra.mv.hom_mv_coe = λ (b : geometric_algebra.hom_mv 0), geometric_algebra.multivector.scalar b

source

@[protected, instance]

def geometric_algebra.mv.has_hom_mv_coe {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

has_coe (geometric_algebra.hom_mv n) (geometric_algebra.multivector n)

Equations

geometric_algebra.mv.has_hom_mv_coe = {coe := geometric_algebra.mv.hom_mv_coe n}

source

@[protected, instance]

def geometric_algebra.mv.has_g0_coe_t {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

has_coe_t G₀ (geometric_algebra.multivector 0)

Equations

geometric_algebra.mv.has_g0_coe_t = {coe := λ (s : G₀), geometric_algebra.mv.hom_mv_coe (geometric_algebra.hom_mv.scalar (geometric_algebra.blade.scalar s))}

source

@[protected, instance]

def geometric_algebra.mv.has_g1_coe_t {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] :

has_coe_t G₁ (geometric_algebra.multivector 1)

Equations

geometric_algebra.mv.has_g1_coe_t = {coe := λ (v : G₁), geometric_algebra.mv.hom_mv_coe (geometric_algebra.hom_mv.vector (geometric_algebra.blade.vector v))}

source

def geometric_algebra.mv.augment_coe {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} (mv : geometric_algebra.multivector n) :

geometric_algebra.multivector n.succ

Equations

geometric_algebra.mv.augment_coe mv = mv.augment 0

source

@[protected, instance]

def geometric_algebra.mv.has_augment_coe {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

has_coe (geometric_algebra.multivector n) (geometric_algebra.multivector n.succ)

Equations

geometric_algebra.mv.has_augment_coe = {coe := geometric_algebra.mv.augment_coe n}

source

@[protected, instance]

def geometric_algebra.mv.has_g0_coe_n {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

has_coe_t G₀ (geometric_algebra.multivector n)

Equations

geometric_algebra.mv.has_g0_coe_n = {coe := n.rec_on coe (λ (n : ℕ) (s : G₀ → geometric_algebra.multivector n) (k : G₀), ↑(s k))}

source

@[protected, instance]

def geometric_algebra.mv.has_g1_coe_n {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

has_coe_t G₁ (geometric_algebra.multivector n.succ)

Equations

geometric_algebra.mv.has_g1_coe_n = {coe := n.rec_on coe (λ (n : ℕ) (s : G₁ → geometric_algebra.multivector n.succ) (k : G₁), ↑(s k))}

source

def geometric_algebra.mv.mv_add {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

geometric_algebra.multivector n → geometric_algebra.multivector n → geometric_algebra.multivector n

Equations

geometric_algebra.mv.mv_add (a.augment ar) (b.augment br) = (geometric_algebra.mv.mv_add a b).augment (ar + br)
geometric_algebra.mv.mv_add (geometric_algebra.multivector.scalar a) (geometric_algebra.multivector.scalar b) = geometric_algebra.multivector.scalar (a + b)

source

@[protected, instance]

def geometric_algebra.mv.has_add {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {n : ℕ} :

has_add (geometric_algebra.multivector n)

Equations

geometric_algebra.mv.has_add = {add := geometric_algebra.mv.mv_add n}

source

def geometric_algebra.fᵥ {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] :

G₁ →+ G

Equations

geometric_algebra.fᵥ = geometric_algebra.f₁ G₀

source

@[reducible]

def geometric_algebra.fₛ {G₀ : Type u} [field G₀] {G : Type u} [ring G] [algebra G₀ G] :

G₀ →+* G

source

def geometric_algebra.prod_vec {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (a b : G₁) :

G

Equations

geometric_algebra.prod_vec a b = ⇑geometric_algebra.fᵥ a * ⇑geometric_algebra.fᵥ b

source

def geometric_algebra.square_vec {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (a : G₁) :

G

Equations

geometric_algebra.square_vec a = geometric_algebra.prod_vec a a

source

def geometric_algebra.sym_prod_vec {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (a b : G₁) :

G

Equations

geometric_algebra.sym_prod_vec a b = geometric_algebra.prod_vec a b + geometric_algebra.prod_vec b a

source

def geometric_algebra.is_orthogonal {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (a b : G₁) :

Prop

Equations

geometric_algebra.is_orthogonal a b = (geometric_algebra.sym_prod_vec a b = 0)

source

theorem geometric_algebra.zero_is_orthogonal {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (a : G₁) :

geometric_algebra.is_orthogonal 0 a

source

@[reducible]

def geometric_algebra.pairwise_ortho_vector {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (r : ℕ) :

Type u

a list of r orthogonal vectors, which may be non-unique

source

def geometric_algebra.is_rblade {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (r : ℕ) (b : G) :

Prop

r-blades

Equations

geometric_algebra.is_rblade r b = ∃ (k : G₀) (v : geometric_algebra.pairwise_ortho_vector r), b = k • (vector.map ⇑geometric_algebra.fᵥ ↑v).to_list.prod

source

def geometric_algebra.Bᵣ {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (r : ℕ) :

set G

Equations

geometric_algebra.Bᵣ r = set_of (geometric_algebra.is_rblade r)

Instances for ↥geometric_algebra.Bᵣ

source

theorem geometric_algebra.Bᵣ.all_G₀_is_rblade0 {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (k : G₀) :

geometric_algebra.is_rblade 0 (⇑geometric_algebra.fₛ k)

source

theorem geometric_algebra.Bᵣ.all_G₁_is_rblade1 {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (a : G₁) :

geometric_algebra.is_rblade 1 (⇑geometric_algebra.fᵥ a)

source

@[protected, instance]

def geometric_algebra.Bᵣ.has_coe_from_G₀ {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] :

has_coe G₀ ↥(geometric_algebra.Bᵣ 0)

Equations

geometric_algebra.Bᵣ.has_coe_from_G₀ = {coe := λ (k : G₀), ⟨⇑geometric_algebra.fₛ k, _⟩}

source

@[protected, instance]

def geometric_algebra.Bᵣ.has_coe_from_G₁ {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] :

has_coe G₁ ↥(geometric_algebra.Bᵣ 1)

Equations

geometric_algebra.Bᵣ.has_coe_from_G₁ = {coe := λ (a : G₁), ⟨⇑geometric_algebra.fᵥ a, _⟩}

source

@[simp]

theorem geometric_algebra.Bᵣ.coe_is_rblade {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] {r : ℕ} (b : ↥(geometric_algebra.Bᵣ r)) :

geometric_algebra.is_rblade r ↑b

source

theorem geometric_algebra.Bᵣ.smul_mem {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] {r : ℕ} {b : G} {k : G₀} (hb : geometric_algebra.is_rblade r b) :

geometric_algebra.is_rblade r (k • b)

source

@[protected, instance]

def geometric_algebra.Bᵣ.mul_action {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (r : ℕ) :

mul_action G₀ ↥(geometric_algebra.Bᵣ r)

Equations

geometric_algebra.Bᵣ.mul_action r = {to_has_smul := {smul := λ (k : G₀) (b : ↥(geometric_algebra.Bᵣ r)), ⟨k • ↑b, _⟩}, one_smul := _, mul_smul := _}

source

@[protected, instance]

def geometric_algebra.Bᵣ.has_neg {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (r : ℕ) :

has_neg ↥(geometric_algebra.Bᵣ r)

Equations

geometric_algebra.Bᵣ.has_neg r = {neg := λ (b : ↥(geometric_algebra.Bᵣ r)), (-1) • b}

source

def geometric_algebra.Gᵣ {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (r : ℕ) :

add_subgroup G

r-vectors

Equations

geometric_algebra.Gᵣ r = add_subgroup.closure (geometric_algebra.Bᵣ r)

Instances for ↥geometric_algebra.Gᵣ

geometric_algebra.Gᵣ.has_scalar

source

theorem geometric_algebra.Gᵣ.smul_mem {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] {r : ℕ} {v : G} {k : G₀} (hv : v ∈ geometric_algebra.Gᵣ r) :

k • v ∈ geometric_algebra.Gᵣ r

source

@[protected, instance]

def geometric_algebra.Gᵣ.has_scalar {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (r : ℕ) :

module G₀ ↥(geometric_algebra.Gᵣ r)

Equations

geometric_algebra.Gᵣ.has_scalar r = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := λ (k : G₀) (v : ↥(geometric_algebra.Gᵣ r)), ⟨k • ↑v, _⟩}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}

source

def geometric_algebra.Mᵣ {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (r : ℕ) :

add_subgroup G

multi-vectors of at most grade r

Equations

geometric_algebra.Mᵣ r = add_subgroup.closure (⋃ (r' : fin r), (geometric_algebra.Gᵣ ↑r').carrier)

source

@[reducible]

def geometric_algebra.is_scalar {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] :

G → Prop

source

theorem geometric_algebra.vec_sym_prod_scalar {G₀ : Type u} [field G₀] {G₁ : Type u} [add_comm_group G₁] [module G₀ G₁] {G : Type u} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G] (a b : G₁) :

geometric_algebra.is_scalar (geometric_algebra.sym_prod_vec a b)

Symmetrised product of two vectors must be a scalar