Zulip Chat Archive

Stream: new members

Topic: Direct sum


view this post on Zulip 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).

view this post on Zulip Thomas Browning (Aug 18 2020 at 06:52):

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

view this post on Zulip 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.)

view this post on Zulip Thomas Browning (Aug 18 2020 at 06:55):

You're right. That was silly.

view this post on Zulip Kyle Miller (Aug 18 2020 at 06:55):

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

view this post on Zulip 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+

view this post on Zulip Eric Wieser (Aug 18 2020 at 09:38):

image.png

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (Aug 18 2020 at 11:00):

DejaVu Sans Mono covers a lot


Last updated: May 09 2021 at 19:11 UTC