## Stream: new members

### Topic: Direct sum

#### Thomas Browning (Aug 18 2020 at 06:51):

I'm having trouble getting the direct sum notation to work.

import linear_algebra.direct_sum_module

noncomputable theory
local attribute [instance, priority 100] classical.prop_decidable

open_locale direct_sum

variables (E : Type*) [field E] (B : set E)
example : B = B :=
begin
have h := @direct_sum.semimodule E _ B _ (λ b, E) _ _,
--have EB := (⊕ (b : B), (λ (x : B), E) b),
--have EB := (⊕ (b : B), E),
refl,
end


Lean doesn't like either of these two attempts at defining EB (the direct sum of B copies of E).

#### Thomas Browning (Aug 18 2020 at 06:52):

The first attempt is a directly copy what lean tells me that h is

#### Kyle Miller (Aug 18 2020 at 06:54):

It's the wrong unicode character.

    have EB := (⨁ (b : B), E),


(At least in emacs, it's \O+ rather than \oplus.)

#### Thomas Browning (Aug 18 2020 at 06:55):

You're right. That was silly.

#### Kyle Miller (Aug 18 2020 at 06:55):

(I still get ∑ and Σ mixed up...)

#### Eric Wieser (Aug 18 2020 at 09:37):

Also silly is how vscode (at least, on windows) renders the n-ary \O+ as smaller than the binary \o+

image.png

#### Scott Morrison (Aug 18 2020 at 10:20):

You can select different fonts in VSCode. Often a font is missing some characters, so I think most people specify several, and VSCode falls back through the list.

I have "Menlo, Monaco, 'Courier New', monospace", but no particular reason to think this is good. (In particular I notice I'm missing the "subscript l" all throughout the linear algebra library, but never fixed it.)

#### Johan Commelin (Aug 18 2020 at 11:00):

DejaVu Sans Mono covers a lot

Last updated: May 09 2021 at 19:11 UTC