Direct sum

Stream: new members

[Thomas Browning]

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]

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

[Kyle Miller]

It's the wrong unicode character.

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

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

[Thomas Browning]

You're right. That was silly.

[Kyle Miller]

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

[Eric Wieser]

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

[Eric Wieser]

image.png

[Scott Morrison]

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]

DejaVu Sans Mono covers a lot