## Stream: general

### Topic: star_ring

#### Scott Morrison (Sep 06 2020 at 07:12):

Do we yet have anything about *-algebras? I'd like some! I know we have src#ring_invo (which I've just tidied up a bit in #4052).

#### Scott Morrison (Sep 06 2020 at 07:14):

I was imagining something like:

variables {R : Type} [ring R] [star_ring R]

example (r s : R) : (r * s)† = s† * r† := ...


#### Scott Morrison (Sep 06 2020 at 07:15):

It would be fun to, e.g. prove Bell's inequality, or define Banach algebras...

#### Frédéric Dupuis (Sep 07 2020 at 00:15):

I think it would be nice to have some sort of has_star typeclass that could be used for this, with instances for complex conjugation, Hermitian adjoints, etc.

#### Scott Morrison (Sep 07 2020 at 03:11):

I wonder how much value has_star itself actually has, vs. starting at star_ring. Are the examples of less-than-rings which we will want to talk about star(=linear, antimultiplicative involutions) on? I guess I have no complaint about star_ring only depending on semiring, rather than ring.

#### Scott Morrison (Sep 07 2020 at 03:12):

I also feel pretty strongly about not making global notation for this. Depending on which topic of mathematics I'm thinking about today, I might feel strongly that this operation should be written as star, bar, or dagger. :-)

#### Johan Commelin (Sep 07 2020 at 04:21):

But the bar will look funny in unicode, no matter what, right?

#### Scott Morrison (Sep 07 2020 at 04:50):

feeling strongly about notation rarely leads to being happy in lean (or life, for that matter)

#### Alex J. Best (Sep 07 2020 at 05:00):

I was kinda surprised this works to be honest:

variables {K : Type} [field K] (x y : K)
def bar : K → K := sorry
notation ̅ a := bar a
#check ̅x
#check ̅(1 : K)


of course the second one looks silly, but  ̅x isn't so bad in vscode.

#### Frédéric Dupuis (Sep 07 2020 at 23:17):

Yeah, actually we probably want to be flexible regarding notation on this one!

#### Eric Wieser (Nov 03 2020 at 14:09):

I've tried to revive the star parts of @Scott Morrison's PR in #4886

#### Frédéric Dupuis (Nov 03 2020 at 16:30):

Were those PRs actually dropped, or did @Scott Morrison just not have time yet?

#### Eric Wieser (Nov 03 2020 at 16:47):

I think he's just been busy

#### Eric Wieser (Nov 03 2020 at 16:48):

I thought I'd try splitting them up to help speed things along

#### Scott Morrison (Nov 04 2020 at 03:47):

I hadn't had time, but definitely come back to them. Happy for any help, however!

#### Eric Wieser (Nov 04 2020 at 10:28):

Should I take that as "I don't object to you splitting out that PR and having to deal with merging it back in later"?

Last updated: May 18 2021 at 17:44 UTC