# Zulip Chat Archive

## Stream: general

### Topic: cross product

#### Johan Commelin (Dec 18 2021 at 10:16):

One of the targets on https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets is the cross product. I agree that it is quite easy to define the cross product on `fin 3 → ℝ`

. But presumably that is not the correct generality, and we want to define it on arbitrary 3-dimensional oriented Euclidean spaces, or something like that.

Maybe that's not even the right generality, and we want something else in fact...

If you have an opinion on what the cross product in Lean should look like, please share it here.

#### Yaël Dillies (Dec 18 2021 at 10:17):

<insert some property> Lie bracket?

#### Patrick Massot (Dec 18 2021 at 10:32):

I don't think we should waste time here. If nobody is interested in the generalization then let's do the specific undergrad case and it will be refactored if anyone needs a generalization in the future. The optimal thing to do now is probably the case of an oriented three dimensional real inner product space, and it would be nice to make sure this applies to `fin 3 → ℝ`

.

#### Eric Wieser (Dec 18 2021 at 10:43):

Would the binary exterior product be a sensible thing to formalize relating to this?

#### Eric Wieser (Dec 18 2021 at 10:53):

Maybe the binary specialization isn't as useful for the exterior product as it is for the tensor product.

#### Eric Wieser (Dec 18 2021 at 10:54):

I think it would be good to have `cross_alternating : alternating_map R V V (fin 2)`

somewhere.

#### Johan Commelin (Dec 18 2021 at 10:55):

@Patrick Massot Would it be good enough to only deal with the case `fin 3 → ℝ`

?

#### Johan Commelin (Dec 18 2021 at 10:55):

(To be honest, I don't think I've ever used the cross product after some example sheet in my 1st year LinAlg course.)

#### Eric Wieser (Dec 18 2021 at 11:13):

I agree we should probably have the generalization to an inner product space

#### Eric Wieser (Dec 18 2021 at 11:13):

Otherwise we can't use it to talk about the model of polar coordinates `(r, θ, ψ)`

without forcing the user to go via an equiv

#### Patrick Massot (Dec 18 2021 at 11:17):

Honestly, I think we could get away with doing only `fin 3 → ℝ`

. This definition is really nothing important.

#### Eric Wieser (Dec 18 2021 at 11:18):

If we don't do the full generalization, we may as well do `fin 3 → R`

so that we can take a cross product of integer vectors, right?

#### Johan Commelin (Dec 18 2021 at 11:56):

You need some `sin(θ)`

in the definition, right?

#### Joseph Myers (Dec 18 2021 at 12:18):

If you define it for a given basis, an arbitrary `comm_ring`

should work.

If you define it for an orientation without specifying a choice of basis, you need extra structure (such as the real inner product) to make the result (as a vector in the same space as the arguments) depend only on the orientation.

I guess that means that the cross product with respect to a given basis is a sensible thing to define, whether or not we also define it with respect to an orientation and prove how it relates to `sin`

in a real inner product space.

We don't yet have "given an orientation of a real inner product space, there exists an orthonormal basis corresponding to that orientation" (but that's something #10737 is aiming towards, being able to describe how concrete basis / alternating map manipulations relate to orientations).

#### Kevin Buzzard (Dec 18 2021 at 14:09):

Johan Commelin said:

You need some

`sin(θ)`

in the definition, right?

Johan -- the definition is `\lam i, if i = 0 then a(1)*b(1)-a(2)*b(2) else if i = 1 then a(2)*b(0)-a(0)*b(2) else a(0)*b(1)-a(1)*b(0)`

#### Johan Commelin (Dec 18 2021 at 14:11):

Good point!

#### Eric Wieser (Dec 18 2021 at 14:15):

Probably better with `![_, _, _]`

#### Kalle Kytölä (Dec 18 2021 at 18:15):

Is it meaningful to make the cross-product an instance of docs#lie_ring on the type `fin 3 → R`

for `[add_comm_group R]`

?

#### Kalle Kytölä (Dec 18 2021 at 18:16):

I don't know if that plays well with nice notation, though.

#### Eric Rodriguez (Dec 18 2021 at 18:18):

wouldn't you need `(comm_)ring`

? but yes, I'd agree that's sensible and then makes it very easy to state at any level of generality

#### Kalle Kytölä (Dec 18 2021 at 18:24):

I'm not very familiar with the implementation of `lie_ring`

, but I think it has `add_comm_group`

assumption.

By the way, I agree with much of the previous discussion that it is not obvious what generalizations we would care about. The cross product is mathematically a bit odd; I think it is something of a "law of small numbers" that there are not too many antisymmetric bilinear gadgets with Jacobi identity on merely 3 dimensional spaces, and therefore the cross product coincides with many conceptually different things.

But allowing e.g. integer entries seems meaningful, as Eric Wieser pointed out.

#### Kevin Buzzard (Dec 18 2021 at 18:25):

The cross product is an isomorphism of $\mathbb{R}^3$ with $\Lambda^2(\mathbb{R}^3)$ and its existence comes from the coincidence that 3 choose 2 is 3 again.

#### Kalle Kytölä (Dec 18 2021 at 18:26):

One of the coincidences I had in mind, indeed.

#### Kalle Kytölä (Dec 18 2021 at 18:35):

To me, the implementation of cross product as an instance of docs#lie_ring would involve only two potential drawbacks:

- competing instances of
`lie_ring`

on`fin 3 → R`

(although I don't currently see serious competitors) - difficulty to use nice notation (or would
`⁅u, v⁆`

be acceptable as such for the cross product?).

#### Eric Rodriguez (Dec 18 2021 at 19:00):

I meant the definition as Kevin wrote above to work, you need + and * so `comm_ring`

seems like the sensible way to create the instance. The instance could be localised, too

#### Johan Commelin (Dec 18 2021 at 19:18):

Every ring `R`

is a Lie algebra, so `fin 3 → R`

would be the Lie algebra $R^{⊕ 3}$.

#### Johan Commelin (Dec 18 2021 at 19:18):

I think that's what mathlib currently assumes it to be.

#### Patrick Massot (Dec 18 2021 at 19:44):

I don't think we should have a globally registered notation for cross product. This is too specialized.

#### Eric Wieser (Dec 18 2021 at 20:22):

`×₃`

as locale notation?

#### Martin Dvořák (Dec 20 2021 at 08:49):

Is anybody working on it? If not, I'd like to take this task. Since I am a beginner, this looks good for me because it is probably the easiest-to-implement TODO in mathlib right now.

#### Martin Dvořák (Dec 20 2021 at 08:53):

I suppose I would define cross product as a function of the type `(fin 3 → α) → (fin 3 → α)`

and I would prove some trivial properties of it (like anticommutativity). Is there something I should be aware of before I start?

#### Johan Commelin (Dec 20 2021 at 09:00):

I think you should be aware of the above discussion :wink: (There are a tonne of generalizations, but I think the consensus is that it's ok to focus on `fin 3 → R`

for now.)

#### Johan Commelin (Dec 20 2021 at 09:01):

Also, please use `R`

instead of `α`

. It is a useful signal to the reader that `R`

is not some random type, but caries a ring-like structure.

#### Martin Dvořák (Dec 20 2021 at 09:55):

Thank you! So you mean `R`

not `ℝ`

right?

#### Martin Dvořák (Dec 20 2021 at 10:16):

Thanks! Imma do it! I think it will be a great exercise to start with and experience the whole mathlib workflow before I dive into something complicated.

#### Joseph Myers (Dec 20 2021 at 12:44):

Maybe at least bilinearity should be bundled (so `(fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R)`

)?

#### Eric Wieser (Dec 20 2021 at 12:55):

Should we be calling `star`

on the output and requiring `star_ring R`

? https://math.stackexchange.com/q/129227/1896 suggests we probably should.

#### Martin Dvořák (Dec 20 2021 at 12:57):

Joseph Myers said:

Maybe at least bilinearity should be bundled (so

`(fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R)`

)?

What does it mean?

#### Eric Wieser (Dec 20 2021 at 12:59):

It means exactly what Joseph said, that the map is bilinear

#### Eric Wieser (Dec 20 2021 at 12:59):

i.e. linear in both arguments

#### Martin Dvořák (Dec 20 2021 at 13:00):

Yes but what is the syntax `→ₗ[R]`

for?

#### Yury G. Kudryashov (Dec 20 2021 at 13:00):

#### Eric Wieser (Dec 20 2021 at 13:01):

If you type in the full type as above, you can hover over it in vs-code to find out what the syntax means

#### Martin Dvořák (Dec 20 2021 at 13:01):

Thank yall for helping the n00b!

#### Martin Dvořák (Dec 20 2021 at 20:18):

Can I get your feedback on my wip please? This is my first time contributing (not only to Lean/mathlib but also to any open source).

https://github.com/madvorak/mathlib/blob/master/src/linear_algebra/cross_product.lean

#### Andrew Yang (Dec 20 2021 at 20:36):

A quick golf

```
/-- cross product is anti-commutative -/
lemma cross_product_anticomm (v w : fin 3 → R) :
v ×₃ w = - (w ×₃ v) :=
begin
simp [cross_product, mul_comm (v _) (w _)]
end
```

#### Martin Dvořák (Dec 20 2021 at 20:47):

Andrew Yang said:

A quick golf

`/-- cross product is anti-commutative -/ lemma cross_product_anticomm (v w : fin 3 → R) : v ×₃ w = - (w ×₃ v) := begin simp [cross_product, mul_comm (v _) (w _)] end`

Thanks a lot!!!!!

I will try to write more proofs in a similar manner.

#### Kyle Miller (Dec 20 2021 at 20:50):

Going back to the Dec 18 discussion, regarding the correct generalization: I think the cross product is commonly regarded as being a bilinear map on $\mathbb{R}^3$, and anyone who uses generalizations tends not to use the cross product itself.

The property that completely determines the cross product is the triple product: $(u \times v)\cdot w=\det[u\ v\ w]$. The idea is that $w\mapsto \det[u\ v\ w]$ is an element of $(\mathbb{R}^3)^*$, and the dot product lets you take this dual vector and turn it back into a vector.

A general version is that if you have some fixed $\omega\in \Lambda^{k+1}(V)$ when $V$ is an inner product space, you can take vectors $v_1,\dots,v_k\in V$, compute the iterated interior multiplication $i_{v_k}i_{v_{k-1}}\cdots i_{v_1}(\omega)\in V^*$, then dualize using the inner product to get an element of $V$. This defines an alternating linear map $\Lambda^k V\to V$. The $k=2$ case when $\omega$ is the determinant form gives the cross product.

#### Martin Dvořák (Dec 20 2021 at 21:07):

Andrew Yang said:

A quick golf

`/-- cross product is anti-commutative -/ lemma cross_product_anticomm (v w : fin 3 → R) : v ×₃ w = - (w ×₃ v) := begin simp [cross_product, mul_comm (v _) (w _)] end`

Is the part `(v _) (w _)`

needed?

#### Andrew Yang (Dec 20 2021 at 21:08):

Seems that it's not. Lean is smarter than I thought.

#### Martin Dvořák (Dec 20 2021 at 21:10):

Andrew Yang said:

Seems that it's not. Lean is smarter than I thought.

What is the process of finding out that `simp`

with my definition and the only lemma `mul_comm`

is enough?

#### Andrew Yang (Dec 20 2021 at 21:13):

after `simp [cross_product]`

, you will see that the two sides of the equation only differs by some `mul_comm`

.

#### Kyle Miller (Dec 20 2021 at 21:14):

Importantly, even though you could rewrite with `mul_comm`

repeatedly forever, `simp`

will put things into a normal form.

#### Martin Dvořák (Dec 20 2021 at 21:16):

Oh! Now I see that sequence

```
dsimp [cross_product],
simp [mul_comm],
```

accomplishes the goal as well!

#### Kyle Miller (Dec 20 2021 at 21:18):

Btw, you can get it down to just one line with

```
lemma cross_product_anticomm (v w : fin 3 → R) :
v ×₃ w = - (w ×₃ v) :=
by simp [cross_product, mul_comm]
```

Here's another:

```
lemma cross_product_anticomm' (v w : fin 3 → R) :
v ×₃ w + w ×₃ v = 0 :=
by simp [cross_product, add_eq_zero_iff_eq_neg, mul_comm]
```

#### Kyle Miller (Dec 20 2021 at 21:20):

If you add spaces around the notation, you'll get somewhat more legible output in the goal window:

```
local infix ` ×₃ `: 68 := cross_product
local infix ` ⬝ ` : 67 := matrix.dot_product
```

#### Martin Dvořák (Dec 20 2021 at 21:31):

Kyle Miller said:

Going back to the Dec 18 discussion, regarding the correct generalization: I think the cross product is commonly regarded as being a bilinear map on $\mathbb{R}^3$, and anyone who uses generalizations tends not to use the cross product itself.

The property that completely determines the cross product is the triple product: $(u \times v)\cdot w=\det[u\ v\ w]$. The idea is that $w\mapsto \det[u\ v\ w]$ is an element of $(\mathbb{R}^3)^*$, and the dot product lets you take this dual vector and turn it back into a vector.

A general version is that if you have some fixed $\omega\in \Lambda^{k+1}(V)$ when $V$ is an inner product space, you can take vectors $v_1,\dots,v_k\in V$, compute the iterated interior multiplication $i_{v_k}i_{v_{k-1}}\cdots i_{v_1}(\omega)\in V^*$, then dualize using the inner product to get an element of $V$. This defines an alternating linear map $\Lambda^k V\to V$. The $k=2$ case when $\omega$ is the determinant form gives the cross product.

Oh! That is a beautiful motivation!

#### Martin Dvořák (Dec 20 2021 at 21:32):

BTW should we fork this conversation — move my n00bish implementation question to a separate thread?

#### Kyle Miller (Dec 20 2021 at 21:37):

@Martin Dvořák More golfing using a lemma with a questionable proof (it perhaps depends on the definition of `finset.sum`

a bit too much?)

```
lemma dot_product_unfold' (v w : fin 3 → R) :
v ⬝ w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2 :=
begin
simp [matrix.dot_product, add_assoc],
rw ← add_zero (v 2 * w 2),
refl,
end
lemma cross_product_perpendicular_first_arg (v w : fin 3 → R) :
v ⬝ (v ×₃ w) = 0 :=
begin
simp only [cross_product, dot_product_unfold'],
simp [mul_sub, mul_assoc, mul_left_comm],
end
```

#### Kyle Miller (Dec 20 2021 at 21:41):

There's a nonterminal simp here, but that lemma is useful for the triple product permutation lemma:

```
lemma triple_product_equality (u v w : fin 3 → R) :
u ⬝ (v ×₃ w) = v ⬝ (w ×₃ u) :=
begin
simp only [cross_product, dot_product_unfold'],
simp [mul_sub, mul_assoc, mul_left_comm, mul_comm],
ring,
end
```

#### Yakov Pechersky (Dec 20 2021 at 21:42):

You can always use docs#finset.sum_univ_succ or whatever it's called

#### Kyle Miller (Dec 20 2021 at 21:43):

This works, too:

```
lemma triple_product_equality (u v w : fin 3 → R) :
u ⬝ (v ×₃ w) = v ⬝ (w ×₃ u) :=
begin
simp only [cross_product, dot_product_unfold',
matrix.head_cons, matrix.cons_vec_bit0_eq_alt0, matrix.empty_append, matrix.cons_val_one,
matrix.cons_vec_alt0, matrix.cons_append, matrix.cons_val_zero],
ring,
end
```

#### Kyle Miller (Dec 20 2021 at 21:44):

@Yakov Pechersky Great:

```
lemma dot_product_unfold' (v w : fin 3 → R) :
v ⬝ w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2 :=
by simp [matrix.dot_product, add_assoc, fin.sum_univ_succ]
```

#### Martin Dvořák (Dec 20 2021 at 21:46):

Do you still want me to create the PR in the end, even tho most of the code is yours?

#### Martin Dvořák (Dec 20 2021 at 21:48):

Ye deserve the credit but I actually wanted to experience the whole workflow with Lean/mathlib. So I don't know now.

#### Arthur Paulino (Dec 20 2021 at 21:51):

Martin Dvořák said:

Ye deserve the credit but I actually wanted to experience the whole workflow with Lean/mathlib. So I don't know now.

There's an "Authors" field at the top of `mathlib`

files. You can credit Kyle and yourself there in alphabetic order. I've done if before and it was fine :smile:

#### Martin Dvořák (Dec 20 2021 at 21:52):

OK! And copyright goes to?

#### Kyle Miller (Dec 20 2021 at 21:53):

@Martin Dvořák Please create the PR! Creating the PR and shepherding it through the review process is a large part of the work.

#### Arthur Paulino (Dec 20 2021 at 21:53):

Martin Dvořák said:

OK! And copyright goes to?

You're creating the file so I think it's you :+1:

#### Martin Dvořák (Dec 20 2021 at 21:54):

OK ok. But I should sort out the `→ₗ[R]`

first, right?

#### Kyle Miller (Dec 20 2021 at 22:02):

@Martin Dvořák A possible framework. I don't know this part of the library well enough to know if this is the best way to do it though:

```
def cross_product : (fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R) :=
{ to_fun := λ a,
{ to_fun := λ b,
![ (a 1)*(b 2) - (a 2)*(b 1) , (a 2)*(b 0) - (a 0)*(b 2) , (a 0)*(b 1) - (a 1)*(b 0) ],
map_add' := λ a b, begin
sorry
end,
map_smul' := λ c a, begin
sorry
end },
map_add' := λ a b, begin
sorry
end,
map_smul' := λ c a, begin
sorry
end }
```

#### Martin Dvořák (Dec 20 2021 at 23:12):

I made progress.

https://github.com/madvorak/mathlib/blob/master/src/linear_algebra/cross_product.lean

My current problem is that I don't know how to attack goals of this form:

```
⊢ {to_fun := λ (b : fin 3 → R),
![(c • a) 1 * b 2 - (c • a) 2 * b 1, (c • a) 2 * b 0 - (c • a) 0 * b 2, (c • a) 0 * b 1 - (c • a) 1 * b 0],
map_add' := _, map_smul' := _}
= ⇑(ring_hom.id R)
c • {to_fun := λ (b : fin 3 → R), ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0],
map_add' := _, map_smul' := _}
```

#### Martin Dvořák (Dec 20 2021 at 23:14):

Unless I am mistaken, I am on the outside level, hence I need to prove equality of two functions of the type `(fin 3 → R) →ₗ[R] (fin 3 → R)`

.

#### Yaël Dillies (Dec 20 2021 at 23:16):

Have you tried `ext`

?

#### Yury G. Kudryashov (Dec 20 2021 at 23:18):

BTW, we have https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_map.html#linear_map.mk%E2%82%82 for creating bilinear maps.

#### Martin Dvořák (Dec 20 2021 at 23:19):

After `ext`

I see the following goal, which I understand even less:

```
⊢ ⇑{to_fun := λ (b : fin 3 → R), ![(c • a) 1 * b 2 - (c • a) 2 * b 1, (c • a) 2 * b 0 - (c • a) 0 * b 2, (c • a) 0 * b 1 - (c • a) 1 * b 0], map_add' := _, map_smul' := _} x x_1 = ⇑(⇑(ring_hom.id R) c • {to_fun := λ (b : fin 3 → R), ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0], map_add' := _, map_smul' := _}) x x_1
```

#### Yaël Dillies (Dec 20 2021 at 23:20):

Clean it up for you own eyes using `dsimp`

.

#### Martin Dvořák (Dec 20 2021 at 23:21):

Yury G. Kudryashov said:

BTW, we have https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_map.html#linear_map.mk%E2%82%82 for creating bilinear maps.

I don't understand the code. Can I somehow use it to just prove the linearity in the second argument and use the "symmetry"?

#### Yury G. Kudryashov (Dec 20 2021 at 23:31):

No, it's not about (anti)symmetric maps. You can use

```
def cross_product : (fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R) :=
linear_map.mk₂
(λ a b, ![...]) -- same is in your code
_
_
_
_
```

This way you don't need to use `linear_map.ext`

#### Martin Dvořák (Dec 20 2021 at 23:55):

[crowdproving]

Well, this is my current state of the proof:

```
⊢ ![c * (a 1 * b 2 - a 2 * b 1), c * (a 2 * b 0 - a 0 * b 2), c * (a 0 * b 1 - a 1 * b 0)] x
= c * ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0] x
```

On the LHS, the vector gets first multiplied and then the element gets selected.

On the RHS, the element first gets selected and then it is multiplied.

image.png

Any idea how to close the goal?

#### Yaël Dillies (Dec 21 2021 at 00:01):

Move multiplication inside, then use extensionality.

#### Martin Dvořák (Dec 21 2021 at 00:03):

What do you mean by "inside" please?

#### Yaël Dillies (Dec 21 2021 at 00:03):

inside the vector

#### Martin Dvořák (Dec 21 2021 at 00:10):

I should probably be trivial, but I am lost. I am probably too tired. Imma continue tomorrow.

#### Eric Rodriguez (Dec 21 2021 at 00:15):

Can you post your code again? A few incantations of `simp`

should really get you there.

#### Yaël Dillies (Dec 21 2021 at 00:16):

Try `rw pi.const_mul`

or something.

#### Eric Wieser (Dec 21 2021 at 00:29):

`fin_cases x; simp`

ought to work

#### Joseph Myers (Dec 21 2021 at 01:49):

Rather than using `![]`

I'd suggest `λ i, a (i + 1) * b (i + 2) - a (i + 2) * b (i + 1)`

and then hopefully you don't need to use `fin_cases`

.

#### Martin Dvořák (Dec 21 2021 at 10:41):

Eric Wieser said:

`fin_cases x; simp`

ought to work

It works! Awesome! Thanks a lot!

Also `fin_cases x; refl,`

works as well, so I will keep the latter.

#### Martin Dvořák (Dec 21 2021 at 11:39):

With your great help, I finished the proofs! What do you think?

https://github.com/madvorak/mathlib/blob/master/src/linear_algebra/cross_product.lean

#### Martin Dvořák (Dec 21 2021 at 11:56):

In the lemmata (everything that follows after line 58), I should rename the arguments to `x`

and `y`

in order to comply with the mathlib's manual of style, right?

#### Martin Dvořák (Dec 21 2021 at 11:57):

However, I don't understand what Jeremy Avigad meant by writing that `a`

, `b`

, `c`

are for propositions.

https://leanprover-community.github.io/contribute/style.html

#### Arthur Paulino (Dec 21 2021 at 12:01):

On formatting style, check how curly brackets are used in other proofs.

I also see some glossary#non-terminal-simp usages, which is avoided in mathlib

#### Martin Dvořák (Dec 21 2021 at 12:01):

Thank you! I will revise it.

#### Arthur Paulino (Dec 21 2021 at 12:11):

This link contains some useful information about documentation: https://leanprover-community.github.io/contribute/doc.html

Your file is currently missing a module documentation, which summarizes what you're exploring, a somewhat precise overview of the main definitions you're proposing and, if applicable, a few `#TODO`

items for next steps.

We usually don't add documentation for lemmas/theorems, although I think this is not forbidden. The motivation is that we try to make the lemmas names precise and explicit enough.

#### Patrick Massot (Dec 21 2021 at 12:19):

Arthur Paulino said:

We usually don't add documentation for lemmas/theorems

I think you got this impression from reading only elementary lemmas in mathlib.

#### Patrick Massot (Dec 21 2021 at 12:19):

What is useless is adding a docstring which takes longer to read than the actual statement.

#### Martin Dvořák (Dec 21 2021 at 12:19):

Did I name my lemmata well?

#### Patrick Massot (Dec 21 2021 at 12:20):

Arthur, you can have a look at https://leanprover-community.github.io/mathlib_docs/analysis/calculus/parametric_interval_integral.html for instance. Lemmas there have quite a number of assumptions and docstrings help a bit.

#### Patrick Massot (Dec 21 2021 at 12:22):

Looking at this page myself, I have a question for @Rob Lewis: why do we get all those `«μ»`

instead of `μ`

?

#### Arthur Paulino (Dec 21 2021 at 12:22):

Patrick Massot said:

Arthur, you can have a look at https://leanprover-community.github.io/mathlib_docs/analysis/calculus/parametric_interval_integral.html for instance. Lemmas there have quite a number of assumptions and docstrings help a bit.

Nice! There's even an explanation for the reasoning behind the proof itself. I was wondering if it was a thing in mathlib

#### Arthur Paulino (Dec 21 2021 at 12:24):

Oh wait, the docstring doesn't explain the proof. Nevermind. But it does help understanding the assumptions

#### Patrick Massot (Dec 21 2021 at 12:26):

We also have complicated proofs having comments explaining the strategy (and such comments can also be found in module docstrings).

#### Patrick Massot (Dec 21 2021 at 12:26):

Have a look at https://github.com/leanprover-community/mathlib/blob/2ceda7850a0aaa35f31697072c755fb3de3dbaa7/src/topology/metric_space/baire.lean#L42 for instance.

#### Eric Wieser (Dec 21 2021 at 12:47):

The weird brackets are because somewhere μ is defined as notation, and the brackets say "not the notation"

#### Patrick Massot (Dec 21 2021 at 12:50):

But this notation is clearly not in scope here.

#### Eric Wieser (Dec 21 2021 at 12:51):

All `open_locale`

notation is in scope in doc-gen

#### Kyle Miller (Dec 21 2021 at 14:18):

@Martin Dvořák I got rid of the nonterminal simps and got things somewhat more mathlib ready. I tried speeding up some of the proofs using some specialized lemmas for operations on 3-vectors (`vec3_eq`

, `vec3_add`

, and so on). I also switched the definition of `cross_product`

to Yury's suggestion and created a locale for vector notation.

There's also the determinant characterization of the triple product:

```
lemma triple_product_eq_det (u v w : fin 3 → R) : u ⬝ (v ×₃ w) = matrix.det ![ u, v, w ]
```

Code:

```
/-
Copyright (c) 2021 Martin Dvorak. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Martin Dvorak, Kyle Miller, Eric Wieser, Andrew Yang
-/
import data.matrix.basic
import data.matrix.notation
import tactic.fin_cases
import linear_algebra.bilinear_map
import linear_algebra.matrix.determinant
/-!
# Cross products
This module defines the cross product of vectors in $R^3$ for $R$ a commutive ring.
## Main definitions
* `cross_product` is the cross product of pairs of vectors in $R^3$.
## Main results
* `triple_product_eq_det`
## Notation
The locale `vectors` gives the following notations:
* `×₃` for the cross product
* `⬝` for dot products
## Tags
cross product
-/
variables {R : Type*}
lemma vec3_eq {a b : fin 3 → R}
(h0 : a 0 = b 0) (h1 : a 1 = b 1) (h2 : a 2 = b 2) :
a = b :=
by { ext x, fin_cases x; assumption }
lemma vec3_eq' {a0 a1 a2 b0 b1 b2 : R}
(h0 : a0 = b0) (h1 : a1 = b1) (h2 : a2 = b2) :
![a0, a1, a2] = ![b0, b1, b2] :=
by rw [h0, h1, h2]
variables [comm_ring R]
lemma vec3_add {a b : fin 3 → R} :
a + b = ![a 0 + b 0, a 1 + b 1, a 2 + b 2] :=
by { apply vec3_eq; refl }
lemma vec3_add' {a0 a1 a2 b0 b1 b2 : R} :
![a0, a1, a2] + ![b0, b1, b2] = ![a0 + b0, a1 + b1, a2 + b2] :=
by { rw vec3_add, refl }
/-- The cross product of two vectors in $R^3$ for $R$ a commutative ring. -/
def cross_product : (fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R) :=
begin
apply linear_map.mk₂ R (λ (a b : fin 3 → R),
![ (a 1)*(b 2) - (a 2)*(b 1) ,
(a 2)*(b 0) - (a 0)*(b 2) ,
(a 0)*(b 1) - (a 1)*(b 0) ]);
intros;
simp only [vec3_add', pi.add_apply, algebra.id.smul_eq_mul, matrix.smul_cons,
matrix.smul_empty, pi.smul_apply];
apply vec3_eq';
ring
end
localized "infixl ` ×₃ `: 68 := cross_product" in vectors
localized "infix ` ⬝ ` : 67 := matrix.dot_product" in vectors
lemma cross_product_def (a b : fin 3 → R) :
a ×₃ b = ![ (a 1)*(b 2) - (a 2)*(b 1) ,
(a 2)*(b 0) - (a 0)*(b 2) ,
(a 0)*(b 1) - (a 1)*(b 0) ] := rfl
lemma cross_product_anticomm (v w : fin 3 → R) :
v ×₃ w = - (w ×₃ v) :=
by simp [cross_product_def, mul_comm]
lemma cross_product_anticomm' (v w : fin 3 → R) :
v ×₃ w + w ×₃ v = 0 :=
by rw [add_eq_zero_iff_eq_neg, cross_product_anticomm]
lemma cross_product_self_eq_zero_vector (v : fin 3 → R) :
v ×₃ v = 0 :=
by simp [cross_product_def, mul_comm]
lemma vec3_dot_product (v w : fin 3 → R) :
v ⬝ w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2 :=
by simp [matrix.dot_product, add_assoc, fin.sum_univ_succ]
lemma dot_self_cross_product_eq_zero (v w : fin 3 → R) :
v ⬝ (v ×₃ w) = 0 :=
by simp [cross_product_def, vec3_dot_product, mul_sub, mul_assoc, mul_left_comm]
lemma dot_cross_product_self_eq_zero (v w : fin 3 → R) :
w ⬝ (v ×₃ w) = 0 :=
by rw [cross_product_anticomm, matrix.dot_product_neg, dot_self_cross_product_eq_zero, neg_zero]
/-- Cyclic permutations preserve triple product.
See also `triple_product_eq_det`. -/
lemma triple_product_permutation (u v w : fin 3 → R) :
u ⬝ (v ×₃ w) = v ⬝ (w ×₃ u) :=
begin
simp only [cross_product_def, vec3_dot_product, matrix.head_cons, matrix.cons_vec_bit0_eq_alt0,
matrix.empty_append, matrix.cons_val_one, matrix.cons_vec_alt0, matrix.cons_append,
matrix.cons_val_zero],
ring,
end
lemma triple_product_eq_det (u v w : fin 3 → R) :
u ⬝ (v ×₃ w) = matrix.det ![ u, v, w ] :=
begin
simp only [vec3_dot_product, cross_product_def, matrix.det_fin_three,
matrix.head_cons,
matrix.cons_vec_bit0_eq_alt0, matrix.empty_vec_alt0,
matrix.cons_vec_alt0, matrix.vec_head_vec_alt0,
fin.fin_append_apply_zero,
matrix.empty_append, matrix.cons_append,
matrix.cons_val', matrix.cons_val_one, matrix.cons_val_zero],
ring,
end
```

#### Kyle Miller (Dec 21 2021 at 14:22):

By the way, is there a way to make `cross_product`

pretty print properly? The expression `v ×₃ w = - (w ×₃ v)`

prints as `⇑(⇑cross_product v) w = -⇑(⇑cross_product w) v`

.

#### Anne Baanen (Dec 21 2021 at 14:24):

You'll probably want to write out the `coe_fn`

/`⇑`

in the notation, so something like (untested):

```
notation v ` ×₃ ` w := ⇑(⇑cross_product v) w
```

#### Kyle Miller (Dec 21 2021 at 14:32):

I haven't been able to get that to work or any number of permutations... Did you manage, @Eric Wieser?

#### Eric Wieser (Dec 21 2021 at 14:32):

No, I didn't. Is this in a branch / PR somewhere?

#### Kyle Miller (Dec 21 2021 at 14:33):

There's a code snippet of a complete module I posted two messages up.

#### Anne Baanen (Dec 21 2021 at 14:34):

I'm having trouble too. How does src#linear_map.comp do it?

#### Eric Wieser (Dec 21 2021 at 14:34):

My point is that I think this is mature enough that zulip is probably no longer the best place to discuss it, and it would probably make sense for @Martin Dvořák to make a PR

#### Anne Baanen (Dec 21 2021 at 14:34):

Ah right, that's not bundled.

#### Martin Dvořák (Dec 21 2021 at 14:48):

Thank you very much for your helps! I will take care of the PR.

#### Martin Dvořák (Dec 21 2021 at 14:59):

If you say that `triple_product_eq_det`

is the main result, should I denote it as a `theorem`

instead?

#### Kyle Miller (Dec 21 2021 at 15:02):

You can put other main results, too. I just wanted to be sure to include that since it's theoretically important.

#### Martin Dvořák (Dec 21 2021 at 15:02):

Can we keep the identifiers `u`

, `v`

, `w`

as name of vectors (even tho they are probably standard names for universes in Lean/mathlib)?

#### Martin Dvořák (Dec 21 2021 at 15:03):

Kyle Miller said:

You can put other main results, too. I just wanted to be sure to include that since it's theoretically important.

I don't want to exaggerate the importance of the other results. I just wanted to denote it as a `theorem`

unless you are opposed to it.

#### Kyle Miller (Dec 21 2021 at 15:03):

`data.fin.vec_notation`

seems to use `u`

and `v`

for vectors

#### Martin Dvořák (Dec 21 2021 at 15:04):

Kyle Miller said:

`data.fin.vec_notation`

seems to use`u`

and`v`

for vectors

Oh, that's weird. In this file, the identifier `u`

is used in both meanings (globally universe; in arguments a vector).

#### Kyle Miller (Dec 21 2021 at 15:05):

I'm not sure it matters whether it's a `theorem`

or not -- in the docs everything seems to be a `theorem`

anyway -- so feel free to choose how you want.

#### Martin Dvořák (Dec 21 2021 at 15:06):

BTW how did you generate the long list of all lemmata used in the last simp?

#### Kyle Miller (Dec 21 2021 at 15:06):

In `data.fin.vec_notation`

, `u`

is used as both a universe variable and an argument, too.

#### Kyle Miller (Dec 21 2021 at 15:06):

`simp?`

#### Martin Dvořák (Dec 21 2021 at 15:07):

```
simp only [vec3_dot_product, cross_product_def, matrix.det_fin_three,
matrix.head_cons,
matrix.cons_vec_bit0_eq_alt0, matrix.empty_vec_alt0,
matrix.cons_vec_alt0, matrix.vec_head_vec_alt0,
fin.fin_append_apply_zero,
matrix.empty_append, matrix.cons_append,
matrix.cons_val', matrix.cons_val_one, matrix.cons_val_zero],
```

#### Kyle Miller (Dec 21 2021 at 15:07):

Yeah, I seeded it with the first three and then did `simp? [vec3_dot_product, cross_product_def, matrix.det_fin_three]`

#### Martin Dvořák (Dec 21 2021 at 15:07):

I suppose you didn't write it by hand. Can I first call just `simp`

and then get the list of all used lemmata in it?

#### Martin Dvořák (Dec 21 2021 at 15:07):

Thanks!

#### Martin Dvořák (Dec 21 2021 at 15:08):

And is there any semantics in which lemmata you placed on the same line?

#### Kyle Miller (Dec 21 2021 at 15:09):

I mostly made sure the three main ones came first in case someone wanted to regenerate it later, and any other rearrangements I might have made don't matter.

#### Damiano Testa (Dec 22 2021 at 07:58):

Just a very minor comment: should

```
lemma cross_product_anticomm (v w : fin 3 → R) :
v ×₃ w = - (w ×₃ v) :=
```

be formulated with the minus sign on the other side of the equality?

```
-- The right-hand side is "easier" than the left-hand side
lemma cross_product_anticomm (v w : fin 3 → R) :
- (v ×₃ w) = w ×₃ v :=
```

#### Yaël Dillies (Dec 22 2021 at 08:18):

That seems nicer, yeah.

#### Martin Dvořák (Dec 22 2021 at 08:55):

Thanks for the suggestion! I updated the pull request.

#### Martin Dvořák (Jan 03 2022 at 12:34):

Anne Baanen said:

You'll probably want to write out the

`coe_fn`

/`⇑`

in the notation, so something like (untested):`notation v ` ×₃ ` w := ⇑(⇑cross_product v) w`

Should I change the notation for ` ×₃ `

to the above? I don't know what `coe_fn`

and `⇑`

mean.

#### Martin Dvořák (Jan 03 2022 at 12:35):

This is the pull request: https://github.com/leanprover-community/mathlib/pull/11181

#### Anne Baanen (Jan 03 2022 at 12:41):

I understood that my suggestion did not work. Does `cross_product v w`

pretty-print as `v ×₃ w`

now?

#### Martin Dvořák (Jan 03 2022 at 12:47):

No, it doesn't. And it is weird. I think that it did pretty print a few commits ago...

#### Martin Dvořák (Jan 03 2022 at 12:58):

It worked when it was written as:

```
local infix ` ×₃ `: 68 := cross_product
```

No it doesn't work when it is written as:

```
localized "infixl ` ×₃ `: 68 := cross_product" in vectors
```

#### Martin Dvořák (Jan 03 2022 at 13:00):

I don't know how it works so it is still possible that the pretty print stopped due to some other change.

#### Martin Dvořák (Jan 03 2022 at 13:01):

Should I experiment with that? Or do you see it from your knowledge?

#### Anne Baanen (Jan 03 2022 at 13:14):

I don't know much about the pretty-printer, and can't think of any other tricks to experiment with. I guess let's just keep it as it is.

#### Kyle Miller (Jan 03 2022 at 16:56):

@Martin Dvořák I'm pretty sure it stopped working when we made `cross_product`

be a multilinear map rather than a plain function.

All `localized`

really does is store the quoted code so that when you later do `open_locale vectors`

it will automatically run `local infixl `

×₃ `: 68 := cross_product`

, so I'd be surprised if that's the cause.

#### Martin Dvořák (Jan 03 2022 at 18:08):

Kyle Miller said:

Martin Dvořák I'm pretty sure it stopped working when we made

`cross_product`

be a multilinear map rather than a plain function.

Oh, you are absolutely right!

#### Eric Wieser (Jan 04 2022 at 12:00):

Instead of providing a bilinear map, would it make more sense to provide the cross product as a `lie_ring`

instance?

#### Johan Commelin (Jan 04 2022 at 12:01):

There is already a `lie_ring`

instance on `fin 3 → ℝ`

. (And it's not propeq to the cross product.)

#### Eric Wieser (Jan 04 2022 at 12:01):

Something like:

```
instance vec3_has_bracket : has_bracket (fin 3 → R) (fin 3 → R) :=
{ bracket := λ u v, u ×₃ v }
instance vec3_lie_ring : lie_ring (fin 3 → R) :=
{ add_lie := linear_map.map_add₂ _,
lie_add := λ u, linear_map.map_add _,
lie_self := cross_product_self,
leibniz_lie := λ u v w, begin
dsimp only [has_bracket.bracket, cross_product_apply],
ext i,
fin_cases i; norm_num; ring,
end,
..pi.add_comm_group }
-- pretty printer can't use this unfortunately
localized "infixl ` ×₃ `: 68 := @has_bracket.bracket _ _ vec3_has_bracket" in vectors
```

#### Eric Wieser (Jan 04 2022 at 12:01):

Johan Commelin said:

There is already a

`lie_ring`

instance on`fin 3 → ℝ`

.

Where? `apply_instance`

didn't find it for me.

#### Johan Commelin (Jan 04 2022 at 12:02):

Weird. Maybe `lie_ring.pi`

is missing from mathlib? But it certainly exists in the platonic ideal of mathlib.

#### Eric Wieser (Jan 04 2022 at 12:02):

Ah, missing import

#### Eric Wieser (Jan 04 2022 at 12:03):

docs#lie_ring.of_associative_ring

#### Damiano Testa (Jan 04 2022 at 12:14):

This seems a situation where a human being told of a Lie bracket on `fin 3 → ℝ`

would not choose the one coming from the instance... or where they would at least ask "Are you really sure that you want the zero Lie-bracket?" :smile:

#### Damiano Testa (Jan 04 2022 at 12:15):

Is it possible to override the instance when the associative ring is also commutative?

#### Johan Commelin (Jan 04 2022 at 12:18):

I'm afraid that's non-trivial.

#### Oliver Nash (Jan 04 2022 at 12:19):

And not desirable; we want to be able to make statements like docs#commutative_ring_iff_abelian_lie_ring

#### Eric Wieser (Jan 04 2022 at 12:25):

I guess a type synonym would solve the problem here

#### Eric Wieser (Jan 04 2022 at 12:28):

Do people agree that working with a lie structure would be better than just having a bilinear map?

#### Oliver Nash (Jan 04 2022 at 12:32):

It's such a specific case that it's hard to have strong feelings. Regarding the cross product as a Lie bracket is mostly just a curiosity. I'd be happy either way.

#### Johan Commelin (Jan 04 2022 at 12:34):

I have never used the cross product apart from the Intro to Calculus course. So I wouldn't put it high up my prio list. But I'm just one anecdote.

#### Damiano Testa (Jan 04 2022 at 12:36):

I also do not have strong opinions, really. If someone asked me to provide a Lie bracket on `ℝ^3`

, my first reaction would probably be "What a weird question". Then I would think about the cross-product. Finally I would think of the zero Lie bracket.

#### Oliver Nash (Jan 04 2022 at 12:38):

I look forward to a long thread about the seven-dimensional cross product once we finish here :-)

#### Ruben Van de Velde (Jan 04 2022 at 12:41):

But that's the last one, right?

#### Johan Commelin (Jan 04 2022 at 12:42):

Damiano Testa said:

If someone asked me to provide a Lie bracket on

`ℝ^3`

,

The standard $\mathfrak{sl}_2$-triple with basis $(X,H,Y)$.

#### Damiano Testa (Jan 04 2022 at 13:35):

Oh, but that is $\mathfrak{sl}_2$, nor $\mathbb{R}^3$: as the notation suggests, they are not the same! :upside_down:

#### Johan Commelin (Jan 04 2022 at 13:37):

Sure, I completely agree. But still, if you ask me to put a Lie algebra structure on a 3-dimensional space with a distinguished basis, this is the one I would pick :smile:

#### Kyle Miller (Jan 04 2022 at 16:05):

Oliver Nash said:

It's such a specific case that it's hard to have strong feelings. Regarding the cross product as a Lie bracket is mostly just a curiosity. I'd be happy either way.

I think it's sort of a curiosity, too, a sort of "law of small numbers" (that there are interesting coincidences for things of small cardinality or dimension).

It does have some sense to it, but it takes a few isomorphisms. We start with $V=\mathbb{R}^3$ as the fundamental $\mathfrak{so}(3)$-module. The adjoint representation is $\Lambda^2 V$, which is isomorphic to $\mathfrak{so}(3)$ since it may be regarded as being antisymmetric matrices (we identify $V$ with $V^*$ using the inner product from the definition for $\mathfrak{so}(3)$). Then, the Hodge star gives an isomorphism $V=\Lambda^2 V$. Through these isomorphims you can transport the Lie bracket for $\mathfrak{so}(3)$ to $\mathbb{R}^3$.

You can also consider the constant part of differential forms on $\mathbb{R}^3$ under wedge product, using the Hodge star to identify 2-forms with 1-forms. This is the significance of cross products in 3D vector calculus.

#### Kyle Miller (Jan 04 2022 at 16:06):

@Johan Commelin What, you wouldn't choose the Heisenberg Lie algebra? :smile:

#### Johan Commelin (Jan 04 2022 at 16:48):

Nah, I'm a semisimple guy

#### Kalle Kytölä (Jan 04 2022 at 21:22):

I almost thought "simple guy" based on the $\R^3 = \mathfrak{sl}_2$ example above, until... :light_bulb: I remembered that we should strive for the mathlib level of generality.

#### Kalle Kytölä (Jan 04 2022 at 21:22):

Ok, bad jokes aside... (Unless the following is yet another one...)

I originally suggested `lie_ring`

for the cross product, because I thought one would then nicely get for free any API consequences of antisymmetry and Jacobi identity. The problems pointed out back then were at least competing `instance`

s (the zero bracket, which I think indeed begs the "are you sure?" question to humans) and perhaps notation (I wasn't sure about it). Also the later proposal of implementing the cross product as a bilinear map for sure gives a substantial amount of API for free.

But in fact `lie_algebra R`

(for `[comm_ring R]`

) should in principle give all API of bilinearity, antisymmetry, and Jacobi identity. So in terms of reusing the maximal amount of existing API, wouldn't it be close to optimal? Except, of course, if getting access to the API requires that `lie_algebra`

is an `instance`

, in which case we only get all the consequences of bilinearity, antisymmetry, and Jacobi identity for the the zero Lie bracket ("for free" :smiley:).

#### Kalle Kytölä (Jan 04 2022 at 21:27):

Just to clarify, that is not a proposal to change anything implemented right now! But since Eric Wieser brought up the possibility of `lie_ring`

implementation again, I thought it might be worth still clarifying what are the merits of the different choices.

#### Eric Wieser (Jan 04 2022 at 23:19):

@Kalle Kytölä, I didn't see your original suggestion, but your comment above nicely summarizes why I think using the `lie`

spelling might be a good idea. Indeed, there's no need to change the approach in the current PR, but it certainly gives us a large pile of reusable lemmas.

#### Kyle Miller (Jan 05 2022 at 00:14):

@Eric Wieser What do you mean specifically by a "`lie`

spelling"?

@Kalle Kytölä Are you aware that the current version of #11181 contains a `lie_ring`

implementation as a local instance? Design-wise, I think it's a nice idea to use the `lie_ring`

instance to prove lemmas that are generally true for Lie rings, but in terms of cross product notation.

I think it's good to consider the principle "just because something is something doesn't mean that it *is* something." I don't see any benefit to be had defining the cross product through the $\mathfrak{so}(3)$ or $\mathfrak{sl}(2)$ exceptional isomorphisms, or requiring that $\mathbb{R}^3$ be a Lie ring and that the cross product needs to be rendered as a Lie bracket. Similarly, the cross product corresponds to the imaginary part of one of the Hurwitz algebras (equivalently: the imaginary part for the quaternions), but do we need to give $\mathbb{R}^3$ a `has_mul`

for a nonunital nonassociative algebra structure? (That would conflict with the `has_mul`

from the pi instance anyway.)

#### Kyle Miller (Jan 05 2022 at 00:18):

There are some exceptional identities involving cross products and dot products that would be nice to have at some point. You can understand them as coming from the representation theory of $\mathbb{R}^3$ as a Lie algebra, but they're also straightforward to prove by algebraic manipulation.

*Edit:* The main one would be $(u\times v)\cdot (w\times x) = (u\cdot w)(v\cdot x) - (u\cdot x)(v\cdot w)$

#### Eric Wieser (Jan 05 2022 at 00:19):

Kyle Miller said:

Eric Wieser What do you mean specifically by a "

`lie`

spelling"?

I mean introduce a type synonym such that instead of having terms of the form `⇑(⇑cross_product v) w`

we have terms of the form `⁅v, w⁆`

. Neither pretty-prints in the nice `×₃`

way anyway, but the latter has more existing lemmas than the former, and is shorter.

#### Eric Wieser (Jan 05 2022 at 00:19):

Perhaps we can reuse the ~~docs#euclidean_space~~ docs#pi_Lp synonym?

#### Eric Wieser (Jan 05 2022 at 00:21):

With the rationale being; `pi_Lp`

replaces the elementwise norm with the Lp norm, just as we want to replace the elementwise bracket with the geometrically meaningful one

#### Kalle Kytölä (Jan 05 2022 at 09:35):

Kyle Miller said:

Kalle Kytölä Are you aware that the current version of #11181 contains a

`lie_ring`

implementation as a local instance? Design-wise, I think it's a nice idea to use the`lie_ring`

instance to prove lemmas that are generally true for Lie rings, but in terms of cross product notation.

Oh, sorry, I had not noticed this! I don't have experience with local instances yet, but I think it is great if this gives access to the `lie_ring`

API. I suppose that since bilinearity is currently more directly built in, a local instance of `lie_algebra`

would not add much? (EDIT: Or would it? With scalars in docs#lie_algebra anything that the`R`

in `fin 3 → R`

is a module over. Might it make a different part of API available, still?)

Kyle Miller said:

I think it's good to consider the principle "just because something is something doesn't mean that it

issomething."

I fully agree! It is only for "free API" reasons I thought the `lie_ring`

or `lie_algebra`

might be appropriate. I have no strong opinions of what the cross product should be fundamentally, but I agree that it is not particularly fundamentally a Lie bracket.

Last updated: Dec 20 2023 at 11:08 UTC