mathlib3 documentation

lean-ga / geometric_algebra.nursery.instances

@[protected, instance]

def field_ga (K : Type u_1) [field K] :

geometric_algebra K K K

Equations

field_ga K = {f₁ := {to_fun := id K, map_zero' := _, map_add' := _}, vec_sq_scalar := _}

@[protected, instance]

def rrc_ga :

geometric_algebra ℝ ℝ ℂ

Equations

rrc_ga = {f₁ := {to_fun := λ (x : ℝ), ↑x, map_zero' := rrc_ga._proof_1, map_add' := rrc_ga._proof_2}, vec_sq_scalar := rrc_ga._proof_3}